Our Reading Group meets each week to discuss papers suggested by our members. Attendance is open to everybody.
Feel free to add paper suggestions to our paper queue. Occasionally,
members give practice talks. Contact Zak to arrange a talk.
- When: Wednesdays at noon
- Where: SE Debugging Room (BA3234)
Current session (2010)
- Oct 27 Impressions of FLoC
- Overview of the different projects that have been/are being carried out by the group.
- Read survey paper on static analysis techniques
- Title: A Survey of Automated Techniques for Formal Software Verification
- Authors: D'Silva, Kroening, Weissenbacher
- This paper appears in: 
- Abstract Interpretation - foundations, applications. Probably will
start by going through existing slides on the topic, then looking at
- Model Checking, CEGAR
- Category Theory: Steve's slides, youtube lectures
- Model Fusion work
- Type Theory, Partial Evaluation
Other topics (not yet ordered)
- Carolyn offered to give a talk at some point on her work on subway systems
- Hybrid Model Checking
- Term Rewriting
- Contracts and concurrency
- Oct 8, 15, 22 David Barton, Notations for systems design
- Oct 1 Shoham Ben-David, Applications of Description Logic and Causality in Model Checking
- Sep 17 Prof. Rick Hehner, a Probability Perspective
- Sep 10 Prof. Rick Hehner, from Boolean Algebra to Unified Algebra
- Sep 3 Aws Albarghouthi, Abstract analysis of concrete execution
- Sep 2 Anya Tafliovich, Predicative Quantum Programming
- Aug 27 Effective
Static Deadlock Detection (Mayur Naik, Chang-Seo Park, Koushik Sen,
David Gay) Winner of ACM SIGSOFT Distinguished Papers Award
- Aug 20 Jianwei Niu, Formal Models for Group-Centric Secure Information Sharing
- Aug 13 Arie Gurfinkel, Decision Diagrams for Linear Arithmetic
- Aug 5 Marsha, partial behavioral models
- July 30 Shoham Ben-David, Explaining Counterexamples Using Causality
- July 23 Aws, On the Use of Planning Technology for Verification
- July 10 Borys Bradel's practice talk, Extending Goal Models with a Probability Model and using Bayesian Networks
- June 26, July 3 Ou went over the slides about abstraction in
software model checking that Marsha and Arie presented in the tutorial
at FM 2006: Model-Checking: From Hardware to Software
- June 5, 19 Talks by Albert: a Practical Theory of Programming, Alternatives to Prof. Hehner's theory
- May 1,8, 29 Byron Cook's TERMINATOR part 1 part 2 part 3 Byron Cook's blog
- Apr 17 Termination Proofs for Systems Code
- Apr 3 Model Checking Programs
- Mar 27 We will continue our review of the Abstract Interpretation slides located at: link
- Mar 20 Practice talk by Anya Tafliovich, Programming with Quantum Communication
- Mar 13 Abstract Interpretation Based Formal Methods and Future Challenges Basic Concepts of Abstract Interpretation
- Mar 6 A Survey of Automated Techniques for Formal Software Verification.
- Feb 13 Jordi Cabot, Verifying UML/OCL Operation Contracts
- Jun 10 Albert Lai talked about operational semantics, soundness of refinements, and lazy evaluation. slides
- May 29 Albert Lai talked about a theorem on loop invariants. slides
- Jan 15 Jocelyn Simmonds talked about using SAT solvers in practice and SAT competitions (using N. Een's FMCAD '07 tutorial slides)
- Jan 8 Jocelyn Simmonds talked about SAT solvers (using N. Een's FMCAD '07 tutorial slides)
- Dec 11 Robert Will talked briefly about Paramodulation
- Dec 4 Albert Lai talked about Rewriting.
- Nov 27 Robert Will described window inference and gave a demo of the Ergo theorem prover.
- Nov 20 Anya Tafliovich described tableaux and model elimination.
- Nov 13 Ric Hehner described resolution.
- Nov 6 Bowen, J.P., Hinchey, M.G. "Ten commandments of formal methods... ten years later", IEEE Computer, Jan. 2006, pp. 40-48.
- Nov 2 Jocelyn Simmonds, "Exploiting Resolution Proofs to
Speed Up LTL Vacuity Detection for BMC" (practice talk for FMCAD),
Planning session for Reading Group (see ReadingGroup#Topic Lists)
- Oct 16 Continued discussing the previous paper (Oct 2)
- Oct 2 O. Grumberg, A. Schuster, A. Yadgar. "3-Valued Circuit
SAT for STE with Automatic Refinement", 5th International Symposium on
Automated Technology for Verification and Analysis (ATVA'07), Tokyo,
October 2007. Paper
- Sept 25 A. Datta, A. Derek, J.C. Mitchell, V. Shmatikov, and
M. Turuani, "Probabilistic polynomial-time semantics for a protocol
security logic" (invited), 32nd International Colloquium on Automata,
Languages and Programming (ICALP '05), Lisbon, July, 2005.
- Sept 18 Jayadev Misra, "Powerlist: A Structure for Parallel Recursion", TOPLAS, Vol. 16, No. 6, pp. 1737-1767, November 1994 (talk)
- Sept 13 Naghmeh Ghafari, "Algorithmic Analysis of Piecewise FIFO Systems" (talk)
- May 9 Kelvin Ku, "Software Model-Checking for Buffer Overflow Analysis: Benchmarking as an Aid to Tool Development" (talk)
- Apr 25 B. Gulavani, T. Henzinger, Y. Kannan, A. Nori and S.
Rajamani. "SYNERGY: a new algorithm for property checking", SIGSOFT
'06/FSE-14: Proceedings of the 14th ACM SIGSOFT International Symposium
on Foundations of Software Engineering
- Apr 4 Mihaela Bobaru, "Finding Environment Guarantees", FASE '07 presentation (talk).
We also read the following paper: Marcelo F. Frias, Carlos G. Lopez
Pombo, and Mariano M. Moscato, "Alloy Analyzer+PVS in the Analysis and
Verification of Alloy Specifications", TACAS '07, Best paper award
- Mar 28 Orna Kupferman and Sarai Sheinvald-Faragy, "Finding
Shortest Witnesses to the Nonemptiness of Automata on Infinite Words",
- Mar 21 K. McMillan, "Lazy Abstraction with Interpolants", CAV'06
- Mar 14 Ranjit Jhala and Kenneth L. McMillan. "A practical
and complete approach to predicate refinement". In TACAS, pages 459-473,
- Mar 7 Ranjit Jhala, Rupak Majumdar, and Ru-Gang Xu, "State of the Union: Type Inference via Craig Interpolation", TACAS '07
- Feb 28 Niklaus Wirth. "Good Ideas, Through the Looking Glass", IEEE Computer, Jan. 2006, pp. 56-68
- Feb 14 (Presented by Kelvin Ku) Himanshu Jain, Franjo
Ivancic, Aarti Gupta, Ilya Shlyakhter, Chao Wang. "Using Statically
Computed Invariants inside the Predicate Abstraction and Refinement
Loop", CAV '06
- Feb 7 Continued discussing the previous paper (Jan 31). Anya
voluteered to look up SERE/PSL, Jocelyn tried to explain LTL testers,
and Mihaela looked into tester composition.
- Jan 31 A. Zaks and A. Pnueli, "PSL Model Checking and Run-time Verification via Testers", FM 06.
- Jan 24 Continued discussing the previous paper (Jan 17)
- Jan 17 Yifeng Chen, "Semantic Inheritance in Unifying Theories of Programming" (referee: Ric)
- Jan 10 Greta Yorsh, Thomas Ball, and Mooly Sagiv, "Testing,
Abstraction, Theorem Proving: Better Together!", International Symposium
on Software Testing and Analysis, 2006
- Dec 13 Continued discussing the previous paper (Dec 6)
- Dec 6 Carroll Morgan, "The Shadow Knows: Refinement of Ignorance in Sequential Programs", MPC 2006
- Nov 29 Caires and Cardelli, "A Spatial Logic for Concurrency (Part I)"
- Nov 22 Lori Clarke and David Rosenblum, "A Historical
Perspective on Runtime Assertion Checking in Software Development", ACM
SIGSOFT Software Engineering Notes, May 2006
- Nov 15 Dershowitz, Hanna, Nadel, "A Scalable Algorithm for Minimal Unsatisfiable Core Extraction", SAT'06
- Nov 8 Rajeev Alur and P. Madhusudan, "Adding Nesting
Structure to Words", Tenth International Conference on Developments in
Language Theory (DLT06) (Invited paper)
- Nov 1 Shiva Nejati, "Thorough Checking Revisited" (practice talk for FMCAD), Yuan Gan, "Runtime Monitoring for Web Services" (talk)
- Oct 25 Beyer, Henzinger and Theoduloz, "Lazy Shape Analysis", CAV 06
- Oct 11 Wonhong Nam and Rajeev Alur, "Learning-based Symbolic
Assume-guarantee Reasoning with Automatic Decomposition", Fourth
International Symposium on Automated Technology for Verification and
- Oct 4 Larsen, Nyman, Wasowski, "Interface Input/Output Automata", FM06
- Sept 27 E.C.R Hehner, "Unified Algebra" (talk)
- Sept 14 Mihaela Bobaru talked about the work she did during her summer internship at NASA
- Jul 20 Kelvin Ku, "Planning under Uncertainty: A Model Based Approach" (talk)
- Jul 13 Steve Easterbrook, "Introduction to Category Theory" (talk). Rick Salay, "Theory of Institutions and Its Applications in Software Engineering" (talk)
- Jul 6 T. Legall, B. Jeannet, and T. Jron, "Verification of
Communication Protocols using Abstract Interpretation of FIFO Queues",
from AMAST 06
- Jun 29 Ji Zhang and Betty Cheng, "Model-Based Development of Dynamically Adaptive Software", (Best paper of ICSE 2006)
- Jun 22 Junfeng Yang, Can Sar, Paul Twohey, Cristian Cadar,
and Dawson Engler, "Automatically generating malicious disks using
symbolic execution" from IEEE Security and Privacy 2006
- Jun 15 Anya Tafliovich, "Predicative Quantum Programming", MPC 2006
- Jun 8 Henk Barendregt, "Introduction to Generalized Type Systems", Journal of Functional Programming, 1(2):124-154, 1991
- Jun 1 David Harel and Bernhard Rumpe, "Meaningful Modeling: What's the Semantics of "Semantics"?", in IEEE Computer, Oct. 2004
- May 25 Corina Pasareanu and Willem Visser, "Verification of
Java Programs Using Symbolic Execution and Invariant Generation", SPIN
- May 9 Continued discussing the previous paper (May 2)
- May 2 Ioannis T. Kassios, "Dynamic Frames: Support for
Framing, Dependencies and Sharing without Restrictions". In J. Misra, T.
Nipkow, E. Sekerinski (eds.) Formal Methods 2006, vol. 4085 of Lecture
Notes in Computer Science, pages 268-283. Springer-Verlag, 2006. Best
- Apr 25 Continued discussing the previous paper (Apr 18)
- Apr 18 Peter W. O'Hearn, John C. Reynolds, and Hongseok Yang, "Local Reasoning about Programs that Alter Data Structures" in CSL 2001
- Apr 11 Dino Distefano, Peter W. O'Hearn, Hongseok Yang, "A Local Shape Analysis Based on Separation Logic", TACAS 2006
- Apr 4 Marsha Chechik and Arie Gurfinkel discussed their
experiences at ETAPS '06. We also read the following paper: Bhargav S.
Gulavani, Sriram K. Rajamani, "Counterexample Driven Refinement for
Abstract Interpretation", TACAS 2006
- Mar 21 Arie Gurfinkel, "Why Waste a Perfectly Good Abstraction?" (practice talk for TACAS '06)
- Mar 14 R. Alur, P. Madhusudan, and Wonhong Nam, "Symbolic Compositional Verification by Learning Assumptions", CAV 2005
- Mar 7 Tamarah Arons, Elad Elster et al, "Formal Verification of Backward Compatibility of Microcode" CAV 2005
- Feb 28 Paper: "Angelic Nondeterminacy as External Choice in CSP" (need more info)
- Feb 21 Arie Gurfinkel, "Supporting Construction, Analysis, and Understanding of Software Models" (talk)
- Feb 14 Edmund Clarke, Muralidhar Talupur, Helmut Veith, "Environment Abstraction for Parameterized Verification", VMCAI 2006
- Jan 31 E.C.R Hehner, "Retrospective and Prospective for Unifying Theories of Programming" (talk)
- Jan 24 Xavier Leroy, "Formal Certification of a Compiler Back-end, or Programming a Compiler with a Proof Assistant", POPL 06
- Jan 17 Corina S. Psreanu, Radek Pelnek and Willem Visser, "Concrete Model Checking with Abstract Matching and Refinement", CAV 2005
- Jan 12 Naghmeh Ghafari and Richard Trefler, "Piecewise FIFO Channels Are Analyzable", VMCAI 2006
- Jan 5 Arie Gurfinkel, "Systematic Construction of Abstractions for Model-Checking" (practice talk for VMCAI 2006)
- Dec 15 Jonathan Amir, "Verification of Web Services" (talk)
- Dec 7 Aysu Betin-Can and Tevfik Bultan, "Interface-based specification and verification of concurrency controllers", SoftMC 2003
- Dec 1 T. Henzinger, R. Jhala, R. Majumdar, "Permissive Interfaces", FSE 2005
- Nov 23 Continued reading a previous paper (Nov 18)
- Nov 18 B. Cook, A. Podelski, and A. Rybalchenko,
"Abstraction Refinement for Termination", SAS 05. Shiva Nejati, Justin
Ward and Jocelyn Simmonds discussed their experiences at ASE '05.
- Nov 10 O. Grumberg, O, Strichman, F. Lerda, and M. Theobald,
"Proof-Guided Underapproximation-Widening for Multi-Process Systems",
- Nov 3 Shiva Nejati and Justin Ward gave practice talks for ASE '05 (talk)
- Oct 26 Leslie Lamport, "Real-time model checking is really simple", CHARME 2005
- Oct 20 Jocelyn Simmonds, practice talk for ASE '05 (talk)
- Oct 12 W.J. Fokkink, J.F. Groote and M.A. Reniers, "Process
algebra needs proof methodology", from The Concurrency Column, Bulletin
of the EATCS, February 2004
- Oct 6 Cindy Eisner, Dana Fisman, and John Havlicek, "A Topological Characterization of Weakness", PODC 2005
- Sept 29 Patrick Maier, "Compositional Circular Assume-Guarantee Rules Cannot Be Sound and Complete", FoSSaCS 2003
Papers are not listed in any particular order. Feel free to add/remove papers/categories.
- E. M. Clarke Jr. "Programming language constructs for which it is
impossible to obtain good Hoare axiom systems", in Journal of the ACM
v26 #1 p129-147, January 1979 (earlier POPL'77) PDF
- B. Moller, "The Linear Algebra of UTP"
- Thomas Ball, Byron Cook, Shuvendu K. Lahiri, and Lintao Zhang.
"Zapato: Automatic theorem proving for predicate abstraction
refinement", in CAV, pages 457-461, 2004
- Arie Gurfinkel and Marsha Chechik. "Why waste a perfectly good abstraction?". In TACAS, pages 212-226, 2006
- Shuvendu K. Lahiri, Randal E. Bryant, and Byron Cook. "A symbolic
approach to predicate abstraction". In CAV, pages 141-153, 2003.
- Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L.
McMillan. "Abstractions from proofs". In POPL, pages 232-244, 2004.
- Ranjit Jhala and Kenneth L. McMillan. "A practical and complete
approach to predicate refinement". In TACAS, pages 459-473, 2006.
- Daniel Kroening and Georg Weissenbacher. "Counterexamples with loops for predicate abstraction". In CAV, pages 152-165, 2006.
- Dzintars Avots, Michael Dalton, V. Benjamin Livshits, and Monica S.
Lam. "Improving software security with a C pointer analysis". In ICSE,
pages 332-341, 2005.
- Manuvir Das, Ben Liblit, Manuel Fähndrich, and Jakob Rehof.
"Estimating the impact of scalable pointer analysis on optimization". In
SAS, pages 260-278, 2001.
- Yichen Xie, Andy Chou, and Dawson R. Engler. "Archer: using
symbolic, path-sensitive analysis to detect memory access errors". In
ESEC / SIGSOFT FSE, pages 327-336, 2003.
- Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérôme Feret,
Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. "A
static analyzer for large safety-critical software". In PLDI, pages
- Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne,
Antoine Miné, David Monniaux, and Xavier Rival. "The astreé analyzer".
In ESOP, pages 21-30, 2005.
- Patrick Cousot and Nicolas Halbwachs. "Automatic discovery of
linear restraints among variables of a program". In POPL, pages 84-96,
- Nurit Dor, Michael Rodeh, and Shmuel Sagiv. "CSSV: towards a
realistic tool for statically detecting all buffer overflows in C". In
PLDI, pages 155-167, 2003.
- Vinod Ganapathy, Somesh Jha, David Chandler, David Melski, and
David Vitek. "Buffer overrun detection using linear programming and
static analysis". In ACM Conference on Computer and Communications
Security, pages 345-354, 2003.
- Brian Hackett, Manuvir Das, Daniel Wang, and Zhe Yang. "Modular
checking for buffer overflows in the large". In ICSE '06: Proceeding of
the 28th international conference on Software engineering, pages
232-241, New York, NY, USA, 2006. ACM Press.
- Antoine Miné. "The octagon abstract domain". In WCRE, pages 310-, 2001.
- John Wilander and Mariam Kamkar. "A comparison of publicly
available tools for static intrusion prevention". In Proceedings of the
7th Nordic Workshop on Secure IT Systems, pages 68-84, Karlstad, Sweden,
Lazy Abstraction and Refinement (BLAST)
- Ranjit Jhala. "Program Verification by Lazy Abstraction". PhD thesis, University of California at Berkeley, 2004.
- Andy Gill and Graham Hutton. "The worker/wrapper transformation".
In preparation for submission to the Journal of Functional Programming,
December 2007. Abstract and PDF
- José Bacelar Almeida and Jorge Sousa Pinto. "Deriving Sorting
Algorithms". Tech Report at Universidade do Minho, Portugal, April 2006.
27 pages. arXiv record
- Sumit Nain and Moshe Vardi. "Branching vs. Linear Time: Semantical Perspective". ATVA'07 invited paper. paper PDF and slides PDF
- Hongwei Xi et al. The ATS dependently-typed programming and proving language. (To be refined to a paper citation or a demo.)
- Leslie Lamport. "The PlusCal Algorithm Language". 2009. Abstract and PDF
- Himanshu Jain, Franjo Ivancic, Aarti Gupta, Ilya Shlyakhter, and
Chao Wang. "Using statically computed invariants inside the predicate
abstraction and refinement loop". In CAV, pages 137-151, 2006.
- Himanshu Jain, Franjo Ivancic, Aarti Gupta, and Malay K. Ganai.
"Localization and register sharing for predicate abstraction". In TACAS,
pages 397-412, 2005.
- Franjo Ivancic, Ilya Shlyakhter, Aarti Gupta, and Malay K. Ganai.
"Model checking c programs using f-soft". In ICCD, pages 297-308, 2005.
- Daniel Kroening, Alex Groce, and Edmund M. Clarke. "Counterexample
guided abstraction refinement via program execution. In Davies et al.
[DSB04], pages 224-238. Formal Methods and Software Engineering, 6th
International Conference on Formal Engineering Methods, ICFEM 2004,
Seattle, WA, USA, November 8-12, 2004, Proceedings, volume 3308 of
Lecture Notes in Computer Science. Springer, 2004.
- Sagar Chaki and Scott Hissam. "Certifying the absence of buffer
overflows". Technical Report CMU/SEI-2006-TN-030, Software Engineering
Institute, Carnegie Mellon University, September 2006.
- Shaunak Chatterjee, Shuvendu K. Lahiri, Shaz Qadeer, and Zvonimir
Rakamaric, "A Reachability Predicate for Analyzing Low-Level Software",
in TACAS '07
- Muhammad Zubair Malik, Aman Pervaiz, and Sarfraz Khurshid,
"Generating Representation Invariants of Structurally Complex Data", in