Conferences
Links
E-Mail:
Byron Cook, Andreas Podelski and Andrey Rybalchenko. Termination Proofs for Systems Code. Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation (PLDI), pages 415-416, 2006, ACM, NY, USA.
Program termination is central to the process of ensuring that systems code can always react. We describe a new program termination prover that performs a path-sensitive and context-sensitive program analysis and provides capacity for large program fragments (i.e. more than 20,000 lines of code) together with support for programming language features such as arbitrarily nested loops, pointers, function-pointers, side-effects, etc.We also present experimental results on device driver dispatch routines from theWindows operating system. The most distinguishing aspect of our tool is how it shifts the balance between the two tasks of constructing and respectively checking the termination argument. Checking becomes the hard step. In this paper we show how we solve the corresponding challenge of checking with binary reachability analysis.
Thursday, November 26th, 2009, 14:00h, Room: ZI 5126.
Shmuel Sagiv, Thomas W. Reps and Reinhard Wilhelm. Parametric Shape Analysis via 3-valued Logic. ACM Transactions on Programming Languages and Systems (TOPLAS), Vol. 24(3), pages 217-298, May 2002, ACM, NY, USA.
Shape analysis concerns the problem of determining "shape invariants" for programs that perform destructive updating on dynamically allocated storage. This article presents a parametric framework for shape analysis that can be instantiated in different ways to create different shape-analysis algorithms that provide varying degrees of efficiency and precision. A key innovation of the work is that the stores that can possibly arise during execution are represented (conservatively) using 3-valued logical structures. The framework is instantiated in different ways by varying the predicates used in the 3-valued logic. The class of programs to which a given instantiation of the framework can be applied is not limited a priori (i.e., as in some work on shape analysis, to programs that manipulate only lists, trees, DAGS, etc.); each instantiation of the framework can be applied to any program, but may produce imprecise results (albeit conservative ones) due to the set of predicates employed.
December, 2009, TBA.
The Formal Methods Reading Group is a group of students and faculty that meets bi-weekly to discuss papers drawn from a broad spectrum of research into formal methods, model checking, program analysis, and concurrency theory.
Papers are mostly recent, but occasionally we include an older "classic". Suggestions are welcome for papers to read. Feel free to add yourself to the mailing list; you can unsubscribe yourself at any time.
Note: the text below is largely based on the description of the PARG meeting format.
The group is informal: we come together to further our understanding of the field. All group members are expected to read the paper, understand it to the best of their ability, and come to the meeting with questions and topics for discussion.
If you haven't read the paper beforehand, you are likely to get much less from the meeting, and also to contribute less to it. However, you don't have to fully understand the paper, or to be an expert in the topic! We encourage researchers of all abilities (from undergrads to faculty) to attend.
Each meeting starts with one group member (the moderator) giving a 5–10 minute overview of the paper. In some sense, moderators just share with the group the notes they made while reading the paper carefully. This sets the background for the rest of the discussion, which consists of people raising the points they noticed when they read the paper, and the group discussing those points.
Here are examples of topics that the moderator (or others) might raise.
Send suggestions for papers to read to the fmrg-discuss mailing list. In case you do not intend to present the paper yourself, you should consider accompanying your suggestion with the name of an alternative moderator (after first asking this person for permission, of course).
Other members of the group are encouraged to send endorsements for proposed papers to the list and pledge their attendance to the meeting.
Discussions about future topics, meeting dates, endorsements, etc. are sent to the fmrg-discuss mailing list. You can subscribe via a web interface, or by sending an empty email to FMRG-DISCUSS-subscribe-request@lists.utwente.nl.
If you want to review previous discussions, there are list archives available.
David Schmidt. Structure-Preserving Binary Relations for Program Abstraction. In The Essence of Computation: Complexity, Analysis, Transformation, T. Mogensen, D. Schmidt, and I. H. Sudburough, editors. Springer LNCS 2566, 2002.
An abstraction is a property-preserving contraction of a program’s
model into a smaller one that is suitable for automated analysis. An
abstraction must be sound, and ideally, complete. Soundness and
completeness arguments are intimately connected to the abstraction
process, and approaches based on homomorphisms and Galois connections
are commonly employed to define abstractions and prove their soundness
and completeness.
This paper develops Mycroft and Jones’s proprosal that an abstraction should be stated as a form of structure-preserving binary relation. Mycroft-Jones-style relations are defined, developed, and employed in characterizations of the homomorphism and Galois-connection approaches to abstraction.
David Schmidt and Bernhard Steffen. Program Analysis as Model Checking of Abstract Interpretations. 5th Static Analysis Symposium, SAS'98 pages 351-380, 1998, Springer.
This paper presents a collection of techniques, a methodology, in which abstract interpretation, flow analysis, and model checking are employed in the representation, abstraction, and analysis of programs. The methodology shows the areas of intersection of the different techniques as well as the opportunites that exist when one technique is used in support of another. The methodology is presented as a three-step process: First, from a (small-step) operational semantics definition and a program, one constructs a program model, which is a state-transition system that encodes the program’s executions. Second, abstraction upon the program model is performed, reducing the detail of information in the model’s nodes and arcs. Finally, the program model is analyzed for properties of its states and paths.
Thursday, December 11th, 14:00h, Room: Citadel H327
A. Prasad Sistla, Patrice Godefroid: Symmetry and Reduced Symmetry in Model Checking. ACM Trans. Program. Lang. Syst. 26(4): 702-734 (2004)
Symmetry reduction methods exploit symmetry in a system in order to efficiently verify its temporal properties. Two problems may prevent the use of symmetry reduction in practice: (1) the property to be checked may distinguish symmetric states and hence not be preserved by the symmetry, and (2) the system may exhibit little or no symmetry. In this article, we present a general framework that addresses both of these problems. We introduce “Guarded Annotated Quotient Structures” for compactly representing the state space of systems even when those are asymmetric. We then present algorithms for checking any temporal property on such representations, including non- symmetric properties.
Wednesday, November 19th, 14:00h, Room: ZI 5126
Guy Gueta, Cormac Flanagan, Eran Yahav and Mooly Sagiv. Cartesian Partial-Order Reduction. Proceedings of SPIN 2007, pages 95-112, June 2007, Springer.
Verifying concurrent programs is challenging since the number of thread interleavings that need to be explored can be huge even for moderate programs. We present a cartesian semantics that reduces the amount of nondeterminism in concurrent programs by delaying unnecessary context switches. Using this semantics, we construct a novel dynamic partial-order reduction algorithm. We have implemented our algorithm and evaluate it on a small set of benchmarks. Our preliminary experimental results show a significant potential saving in the number of explored states and transitions.
Wednesday, November 5th, 2008, 14:00h, Room: ZI 4126.