From SE Wiki
Jump to: navigation, search

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

Topic Lists

Ordered Topics

  • 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: [1]
  • Abstract Interpretation - foundations, applications. Probably will start by going through existing slides on the topic, then looking at papers.
  • Model Checking, CEGAR
  • Terminator
  • 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
  • Pi-calculus
  • Recovery
  • Concurrency
  • Hybrid Model Checking
  • Term Rewriting
  • Contracts and concurrency

Previous Sessions



  • 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", CONCUR '06
  • 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, 2006
  • 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 Analysis (ATVA06)
  • 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 2004
  • 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 paper award.
  • 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", POPL 2005
  • 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

Paper Queue

Papers are not listed in any particular order. Feel free to add/remove papers/categories.

General SE

  • 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.

Alias Analysis

  • 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.

Static Analysis

  • 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 196-207, 2003.
  • 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, 1978.
  • 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.

Tool Comparisons

  • 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, November 2002.

Lazy Abstraction and Refinement (BLAST)

  • Ranjit Jhala. "Program Verification by Lazy Abstraction". PhD thesis, University of California at Berkeley, 2004.

Program Derivation

  • 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 TACAS '07