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)[edit]

Timeline[edit]

Oct 27 Impressions of FLoC

Topic Lists[edit]

Ordered Topics[edit]

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

Previous Sessions[edit]

2009[edit]

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

2008[edit]

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)

2007[edit]

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

2006[edit]

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)

2005[edit]

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[edit]

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

General SE[edit]

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"

Abstraction[edit]

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[edit]

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[edit]

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[edit]

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)[edit]

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

Program Derivation[edit]

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

Miscellaneous[edit]

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

Contents