This repository has been archived by the owner on May 19, 2021. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathdocs.html
65 lines (65 loc) · 5.57 KB
/
docs.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "http://www.w3.org/TR/xhtml11/DTD/xhtml11.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<link rel="icon" type="image/png" href="images/goblint_icon.png" />
<title>Goblint: Papers</title>
<link href="gobstyle.css" rel="stylesheet" type="text/css" />
</head>
<body>
<div id="wrap">
<div id="head">
<div id="inst_logo">
<a href="http://www.cs.ut.ee/eng"><img src="images/TartuLogo.png" alt="Tartu Logo" width="27" height="40" /></a>
<a href="http://www.in.tum.de/en.html"><img src="images/TUMLogo.png" alt="TUM Logo" width="79" height="40" /></a>
</div>
<a href="index.html"><img src="images/goblint.png" alt="Goblint" width="225" height="37" id="goblint" /></a>
<ul id="navbar">
<li><a href="download.html">Download</a></li>
<li><a href="intro.html">Overview</a></li>
<li class="current">Papers</li>
</ul>
</div>
<div id="container">
<h2> Papers related to Goblint</h2>
<ul>
<li><a href="https://link.springer.com/chapter/10.1007/978-3-030-41103-9_5">Incremental Abstract Interpretation</a>. <em>LNCS'20.</em>
Shows how the top-down solver can be employed for the incremental analysis of program code that is undergoing changes.</li>
<li><a href="https://dl.acm.org/doi/abs/10.1145/3236950.3236967">Three Improvements to the Top-Down Solver</a>. <em>PPDP'18.</em>
Describes how the top-down solver can be tuned to deal with non-monotonic right-hand sides, store abstract values only where necessary, and to work with side-effecting constraint systems.</li>
<li><a href="http://dl.acm.org/authorize?N27656">Static race detection for device drivers: the Goblint approach</a>. <em>ASE'16.</em>
This is the definitive overview of Goblint as a static data race analyzer.</li>
<li><a href="http://dx.doi.org/10.1007/978-3-662-53413-7_22">Enforcing Termination of Interprocedural Analysis</a>. <em>SAS'16.</em>
Describes how to make solvers always terminate for interprocedural analysis.</li>
<li><a href="http://goblint.in.tum.de/papers/flags.pdf">Precise Analysis of Value-Dependent Synchronization in Priority Scheduled Programs</a>. <em>VMCAI'14.</em>
Describes how to deal with synchronization using integer variables checked by the programmer.</li>
<li><a href="http://dl.acm.org/authorize?N27657">How to combine widening and narrowing for non-monotonic systems of equations</a>. <em>PLDI'13.</em>
We had long been searching for a way to introduce widening/narrowings into the demand-driven solvers used in Goblint. This paper shows how to do it.</li>
<li><a href="http://goblint.in.tum.de/papers/side.pdf">Side-effecting constraint systems: A Swiss army knife for program analysis</a>. <em>APLAS'12.</em>
Generalizes the global invariant approach to arbitrary side-effecting constraints. This is the theoretical foundation of the Goblint analysis framework.</li>
<li><a href="http://goblint.in.tum.de/papers/class.pdf">Class-modular, class-escape and points-to analysis for object-oriented languages</a>. <em>NFM'12.</em>
Describes a class-escape analysis for C++ implemented in Goblint using LLVM as frontend.</li>
<li><a href="http://dl.acm.org/authorize?N27658">Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol</a>. <em>POPL'11.</em>
Presents the techniques the analyzer uses to analyze OSEK programs.</li>
<li><a href="http://goblint.in.tum.de/papers/coq.pdf">Verifying a Local Generic Solver in Coq</a>. <em>SAS'10.</em>
A verified version of the local solver used in Goblint.</li>
<li><a href="http://goblint.in.tum.de/papers/regions.pdf">Region analysis for race detection</a>. <em>SAS'09.</em>
This paper explains the region analysis method that we use to deal with medium-grained locking.</li>
<li><a href="http://goblint.in.tum.de/papers/must-alias.pdf">A smooth combination of linear and Herbrand equalities for polynomial time must-alias analysis</a>. <em>FM'09. </em>
Presents the key ideas for dealing with per-element locking.</li>
<li><a href="http://goblint.in.tum.de/papers/goblint.pdf">Goblint: path-sensitive data race analysis</a>. <em>SPLST'07.</em>
Overview of the race detection analysis and how it uses property-simulation to obtain a path-sensitive analysis.</li>
<li><a href="http://goblint.in.tum.de/papers/invariants.pdf">Global invariants for analysing multi-threaded applications</a>. <em>NWPT'02.</em>
Describes the underlying nested-fixpoint style thread-modular analysis engine that enables us to analyze multi-threaded programs soundly.</li>
</ul>
<h2> Dissertations related to Goblint</h2>
<ul>
<li><a href="http://www2.in.tum.de/bib/files/Vojdani10Thesis.pdf">Static Data Race Analysis of Heap-Manipulating C Programs.</a> Vesal Vojdani. PhD thesis. University of Tartu, December 2010.</li>
<li><a href="http://www2.in.tum.de/bib/files/apinis14diss.pdf">Frameworks for analyzing multi-threaded C.</a> Kalmer Apinis. PhD thesis. Technische Universität München, June 2014</li>
<li><a href="http://www2.in.tum.de/bib/files/diss-schwarz.pdf">Static Analysis of Embedded Software with Priority Scheduling and Interrupts</a> Martin Schwarz. PhD thesis. Technische Universität München, May 2014</li>
</ul>
</div>
</div>
</body>
</html>