Software Reliability Methods: Readings

This page contains readings on the topics covered by this course. Students will pick from these readings for their in-class presentations.

Course text

  1. Doron Peled: Software Reliability Methods. Springer, 2001.

Background

  1. R. Alur, D.L. Dill. A Theory of Timed Automata. in: Theoretical Computer Science Vol. 126, No. 2, April 1994, pp. 183-236. http://citeseer.ist.psu.edu/alur94theory.html

  2. Beeck, M. von der. A comparison of statecharts variants. In H. Langmaack, W.-P. de Roever, and J. Vytopil, editors, Formal Techniques in Real-Time and Fault-Tolerant Systems, Lecture Notes in Computer Science 863, pages 128--148. Springer-Verlag, 1994.

  3. Gregor Bochmann. Finite State Description of Communication Protocols. Computer Networks, 2:362-372, 1978

  4. E.W. Dijkstra: Cooperating Sequential Processes. EWD 123
    http://www.cs.utexas.edu/users/EWD/ewd01xx/EWD123.PDF 

  5. R. Floyd: Assigning Meaning to Programs. In J. T. Schwartz (ed.):  Proceedings of Symposium on Applied Mathematical Aspects of Computer Science. American mathematical Society, 1967, 19-32.
    http://raw.cs.berkeley.edu/Papers/FloydMeaning.pdf

  6. D. Harel. Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8:231--274, 1987. http://citeseer.ist.psu.edu/harel87statecharts.html

  7. C. A. R. Hoare: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10): 576-580 (1969)
    http://portal.acm.org/citation.cfm?doid=363235.363259

  8. Gerard J. Holzmann: Design and Validation of Computer Protocols. Prentice Hall, 1991
    http://spinroot.com/spin/Doc/Book91.html

  9. Gary Levin, David Gries: A Proof Technique for Communicating Sequential Processes. Acta Inf. 15: 281-302 (1981)

  10. T. Nipkow. Term rewriting and beyond---theorem proving in Isabelle. Formal Aspects of Computing, 1:320--338, 1989

  11. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6(4):319-340, 1976

  12. D. Park. Concurrency and automata on infinite sequences. LNCS 104, pages 167--183, 1981

Safety and Liveness

  1. B. Alpern and F.B. Schneider. Recognizing safety and liveness. Distributed Computing, 2:117.126, 1987.
    http://citeseer.ist.psu.edu/alpern86recognizing.html

  2. A.P. Sistla: Safety, Liveness, and Fairness in Temporal Logic. Formal Aspects of Computing 6(1994), 495.511
    http://citeseer.ist.psu.edu/prasadsistla99safety.html

Formal Models & Model Checking

  1. Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. In 38th Annual Symposium on Foundations of Computer Science, pages 100-109, Miami Beach, Florida, 20-22 October 1997
    http://citeseer.ist.psu.edu/alur97alternatingtime.html

  2. M. Broy: Compositional Refinement of Interactive Systems, No. 89, Digital Systems Research Center, Palo Alto, California, July 1992.
    http://citeseer.ist.psu.edu/article/broy92compositional.html

  3. Manfred Broy, Ingolf Krüger: Interaction Interfaces - Towards a Scientific Foundation of a Methodological Usage of Message Sequence Charts. ICFEM 1998
    http://www4.informatik.tu-muenchen.de/publ/papers/BK98.pdf

  4. M.C. Browne, E.M. Clarke, O. Grumberg: Characterizing Finite Kripke Structures in Propositional Temporal Logic. Theoretical Computer Science, 59 (1,2), 1988, pp. 115-131.

  5. J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang. Symbolic model checking 1020 states and beyond. Information and Computation, 98(2):142--170, June 1992.
    http://citeseer.ist.psu.edu/burch90symbolic.html

  6. K. M. Chandy and J. Misra: Proofs of Networks of Processes
    IEEE, Vol. SE-7, No. 4, pp. 417-426
    http://www.cs.utexas.edu/users/misra/scannedPdf.dir/ProofsNetworks.pdf

  7. E. Allen Emerson, E. M. Clarke: Characterizing correctness properties of parallel programs using fixpoints. In Proceedings of the 7th International Colloquiurn on Automata, Languages, and Programming. Lectures Notes in Computer Science, vol. 85, Springer-Verlag, New York, 1980, pp. 169-181.

  8. Emerson, E. A.: Automated temporal reasoning about reactive systems. In Logics for Concurrency: Structure versus Automata, number 1043 in Lecture Notes in Computer Science. Springer-Verlag. 41.101, 1996.
    http://citeseer.ist.psu.edu/emerson96automated.html

  9. R. Gerth, D. Peled, M. Y. Vardi, and P. Wolper. Simple on-the-fly automatic verification of linear temporal logic. In Proc. 15th Work. Protocol Specification, Testing, and Verification, Warsaw, June 1995. North-Holland.
    http://citeseer.ist.psu.edu/gerth95simple.html

  10. Patrice Godefroid, Sarfraz Khurshid: Exploring Very Large State Spaces Using Genetic Algorithms, J.-P. Katoen and P. Stevens (Eds.): TACAS 2002, LNCS 2280, pp. 266.280, 2002.

  11. Patrice Godefroid, Doron Peled, Mark G. Staskauskas: Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs. ISSTA 1996: 261-269
    http://portal.acm.org/citation.cfm?doid=229000.226324

  12. Patrice Godefroid, Pierre Wolper: Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. Formal Methods in System Design 2(2): 149-164 (1993)

  13. Patrice Godefroid, Pierre Wolper: A Partial Approach to Model Checking. LICS 1991: 406-415

  14. Patrice Godefroid: Using Partial Orders to Improve Automatic Verification Methods. CAV 1990: 176-185

  15. Wilsin Gosti, Tiziano Villa, Alexander Saldanha, Alberto L. Sangiovanni-Vincentelli: An Exact Input Encoding Algorithm for BDDs Representing FSMs. In: Great Lakes Symposium on VLSI '98, IEEE, 1998

  16. Leslie Lamport. The temporal logic of actions. ACM TOPLAS, 16(3):872 . 923, March 1994.
    http://citeseer.ist.psu.edu/lamport90temporal.html  

  17. Manna, Z, and A. Pnueli. How to cook a temporal proof system for your pet language. Proc. of the Symposium on Principles of Programrning Languages, ACM, Austin, Jan. 1983
    http://doi.acm.org/10.1145/567067.567082

  18. Markus Kaltenbach, Jayadev Misra: A Theory of Hints in Model Checking, in Formal Methods at the Crossroads: From Panacea to Foundational Support, ed. Bernhard K. Aichernig and Tom Maibaum, LNCS 2757, pp 423-438, Springer-Verlag, 2003
    http://www.cs.utexas.edu/users/psp/hmc.pdf

  19. Jayadev Misra: A Simple, Object-based View of Multiprogramming,
    Formal Methods in System Design, Vol. 20, No. 1, January 2002
    http://www.cs.utexas.edu/users/psp/ModularMultiprog.pdf

  20. Jayadev Misra: A logic for Concurrent Programming (in two parts): Safety and Progress,
    Journal of Computer and Software Engineering, Vol.3, No.2, pp 239-300, 1995
    http://www.cs.utexas.edu/users/psp/SafetyProgress.pdf

  21. Jayadev Misra: Loosely Coupled Processes, Future Generations Computer Systems 8, 269-286, North-Holland, 1992
    http://www.cs.utexas.edu/users/psp/loosely-coupled.pdf

  22. Doron Peled, Amir Pnueli: Proving Partial Order Properties. TCS 126(2): 143-182 (1994)

  23. A Pnueli. The Temporal Logic of Programs. In Proceedings of the Eighteenth Symposium on the Foundations of Computer Science, 1977

  24. Jean-Pierre Queille and Joseph Sifakis. Specification and verification of concurrent systems in CESAR. In Mariangiola Dezani-Ciancaglini and Ugo Montanari, editors, International Symposium on Programming, 5th Colloquium, volume 137 of Lecture Notes in Computer Science, pages 337--351. Springer, 1982

  25. S. Safra. On the complexity of omega-automata. In Proceedings of the 29th Annual Symposium on Foundations of Computer Science, FoCS'88, pages 319--327, Los Alamitos, California, October 1988. IEEE Computer Society Press

  26. Sistla, A. P., Clarke, E. M., Francez, N., and Meyer, A. R., Can Message Buffers be Axiomatized in Temporal Logic?, Information & Control, vol. 63., nos. 1/2, Oct./Nov. 84, pp. 88-112.

  27. Moshe Y. Vardi, Pierre Wolper: An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report). LICS 1986: 332-344

  28. Pierre Wolper: Expressing Interesting Properties of Programs in Propositional Temporal Logic. POPL 1986: 184-193

  29. Kenneth L. McMillan, Applications of Craig Interpolation to Model Checking , TACAS 05

  30. Patrice Godefroid: Model Checking for Programming Languages using VeriSoft. POPL 1997.

  31. Rajeev Alur and Thomas A. Henzinger: Reactive Modules. Formal Methods in System Design, 1999.

  32. Kenneth L. McMillan: Verification of an Implementation of Tomasulo's Algorithm by Compositional Model Checking CAV 1998.

Type Systems

  1. Luis Damas and Robin Milner: Principal type-schemes for functional programs. ACM POPL 1982: 207-212.

  2. Luca Cardelli: Type Systems. In the Computer Science and Engineering Handbook 1997:2208-2236.

  3. Alexander Aiken: Introduction to Set Constraint-Based Program Analysis. Science of Computer Programming 35(2): 79-111 (1999).

  4. Philip Wadler, Linear types can change the world!, in M. Broy and C. Jones, editors, Programming Concepts and Methods, Sea of Galilee, Israel, April 1990. North Holland, Amsterdam, 1990.

  5. Philip Wadler, A taste of linear logic, Springer Verlag LNCS 802, 1993

  6. M. Tofte and J. Talpin, Implementation of the Typed Call-by-Value Lambda-calculus using a Stack of Regions, POPL 94

  7. Karl Crary, David Walker, Greg Morrisett Typed memory management in a calculus of capabilities, POPL 1999

  8. Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to Typed Assembly Language, TOPLAS 1999

  9. David Walker, A Type System for Expressive Security Policies, POPL 2000

  10. Dan Grossman, Greg Morrisett, Trevor Jim, Florham Park, Michael Hicks, Yanling Wang, James Cheney, Region-Based Memory Management in Cyclone, PLDI 02

  11. Dan Grossman, Existential Types for Imperative Languages, ESOP 2002

  12. Cormac Flanagan, Stephen N. Freund: Type-based race detection for Java. PLDI 2000: 219-232.

  13. Cormac Flanagan and Shaz Qadeer, A Type and Effect System for Atomicity, PLDI 03

  14. Cormac Flanagan, Stephen N. Freund and Marina Lifshin, Type Inference for Atomicity, TLDI 05

  15. Robert O'Callahan, Daniel Jackson: Lackwit: A Program Understanding Tool Based on Type Inference. ICSE 1997: 338-348.

  16. Umesh Shankar, Kunal Talwar, Jeff Foster and David Wagner. Detecting Format-String Vulnerabilities with Type Qualifiers. USENIX Security, 2001.

  17. Frank Pfenning, Hongwei Xi. Dependent Types in Practical Programming USENIX Security, 2001.

Automated Theorem Proving and Applications

  1. George Necula and Peter Lee: Proof-Carrying Code. Proof-Carrying Code. POPL 1996.

  2. Susanne Graf and Hassen Saidi, Construction of Abstract State Graphs of Infinite Systems with PVS, CAV 97

  3. Flanagan, Leino, Lillibridge, Nelson, Saxe, State, Extended Static Checking for Java, PLDI 02

  4. Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani, Automatic Predicate Abstraction of C Programs, PLDI 01

  5. T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre, Lazy Abstraction, POPL 02.

  6. Cormac Flanagan, K. Rustan M. Leino, Mark Lillibridge, Greg Nelson, James B. Saxe, Raymie Stata: Extended Static Checking for Java. PLDI 2002: 234-245.

  7. Cormac Flanagan, Rajeev Goshi, Xinming Ou, and James B. Saxe, Theorem Proving using Lazy Proof Explication, CAV 03

  8. Lerner, Millstein, Rice, Chambers, Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules, POPL 05

  9. Patrice Godefroid, Nils Klarlund, Koushik Sen: DART: Directed Automated Random Testing, PLDI 2005

Program Analysis

  1. P. Cousot and R. Cousot, Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints, POPL 1977.

  2. P. Cousot and R. Cousot, Systematic design of program analysis frameworks, POPL 1979.

  3. Thomas Reps, Susan Horwitz and Mooly Sagiv. Precise Interprocedural Dataflow Analysis via Graph Reachability. POPL 1995.

  4. Mooly Sagiv, Thomas Reps and Reinhard Wilhelm. Parametric Shape Analysis via Three-Valued Logic. ACM Transactions on Programming Languages and Systems, 2002.

  5. Thomas Ball and Sriram Rajamani. Bebop: A Path-sensitive Interprocedural Dataflow Engine.

  6. Carl Gould, Zhendong Su, and Premkumar Devanbu, Static Checking of Dynamically Generated Queries in Database Applications. ICSE 2005.

  7. M. Das, M. Seigle, and S. Lerner, ESP: Path-Sensitive Program Verification in Polynomial Time, PLDI 02.

  8. Jeffrey S. Foster, Tachio Terauchi, and Alex Aiken, Flow-Sensitive Type Qualifiers, PLDI 02

  9. Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro and Thomas Anderson, Eraser: a dynamic data race detector for multithreaded programs, TOCS Nov 1997

  10. Yichen Xie and Alex Aiken, Scalable Error Detection using Boolean Satisfiability, POPL 2005

  11. Westley Weimer and George C. Necula, Finding and Preventing Run-time Error Handling Mistakes, OOPSLA 2004

Real-Time Systems

  1. M. Abadi and L. Lamport. An Old-Fashioned Recipe for Real Time. In Proc. of REX Workshop "Real-Time: Theory in Practice", volume 600 of Lecture Notes in Computer Science, 1993.
    http://citeseer.ist.psu.edu/article/abadi93oldfashioned.html

Synthesis

  1. Haghverdi E. and Ural H.: Submodule Construction from Concurrent System Specifications. Information and Software Technology, (41) 8, 1999, pp. 499-506,
    http://citeseer.ist.psu.edu/haghverdi98submodule.html

  2. I. Krüger, R. Grosu, P. Scholz, M. Broy: From MSCs to Statecharts, in: Franz J. Rammig (ed.): Distributed and Parallel Embedded Systems, Kluwer Academic Publishers, 1999
    http://www4.informatik.tu-muenchen.de/publ/html.php?e=254

  3. S. Uchitel, J. Kramer, J. Magee: Synthesis of Behavioral Models from Scenarios. IEEE Transactions on Software Engineering, Vol. 29, Issue 2, Pages: 99 - 115, 2003
    http://csdl.computer.org/comp/trans/ts/2003/02/e0099abs.htm

Testing

  1. Therese Berg, Olga Grinchtein, Bengt Jonsson, Martin Leucker, Harald Raffelt, and Bernhard Steffen: On the Correspondence Between Conformance Testing and Regular Inference. In: M. Cerioli (Ed.): FASE 2005, LNCS 3442, pp. 175.189, 2005.

  2. Anders Ek, Jens Grabowski, Dieter Hogrefe, Richard Jerome, Beat Koch, Michael Schmitt II: Towards the industrial use of validation techniques and automatic test generation methods for SDL specifications. SDL Forum 1997: 245-260

  3. Elsa L. Gunter, Doron Peled: Using Functional Languages in Formal Methods: The PET System . PDPTA 2000: 2981-2986
    http://www.dcs.warwick.ac.uk/~doron/dblp.html

  4. Elsa L. Gunter, Robert P. Kurshan, Doron Peled: PET: An Interactive Software Testing Tool. CAV 2000: 552-556
    http://www.dcs.warwick.ac.uk/~doron/dblp.html

  5. Elsa L. Gunter, Doron Peled: Path Exploration Tool. TACAS 1999: 405-419
    http://www.dcs.warwick.ac.uk/~doron/dblp.html

  6. Hardi Hungar, Tiziana Margaria, Bernhard Steffen: Test-based Model Generation for Legacy Systems. In: Proceedings of the International Test Conference 2003, 2003

  7. Therese Berg1, Olga Grinchtein1, Bengt Jonsson1, Martin Leucker2, Harald Raffelt3, and Bernhard Steffen3: Domain-Specific Optimization in Automata Learning. In:

  8. D. Lee and M. Yannakakis, Principles and methods of testing finite state machines - a survey, Proc. of the IEEE, vol. 84, pp. 1090--1123, Aug 1996.
    http://citeseer.ist.psu.edu/lee96principles.html

  9. N. Sharygina and D. Peled. A Combined Testing and Verification Approach for Software Reliability. In Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, pages 611-628, 2001
    http://www.dcs.warwick.ac.uk/~doron/dblp.html

Tools

  1. SPIN: http://spinroot.com/spin/whatispin.html

  2. SMV: http://www-2.cs.cmu.edu/~modelcheck/smv.html

  3. NuSMV: http://sra.itc.it/tools/nusmv/index.html

  4. Cadence SMV: http://www-cad.eecs.berkeley.edu/~kenmcmil/smv/

  5. BMC: http://www-2.cs.cmu.edu/~modelcheck/bmc.html

  6. Murphi: http://verify.stanford.edu/dill/murphi.html

  7. CADP: http://www.inrialpes.fr/vasy/cadp.html#Language

  8. PEP: http://theoretica.informatik.uni-oldenburg.de/~pep/

  9. Java Pathfinder: http://ase.arc.nasa.gov/havelund/jpf.html

  10. Bandera: http://bandera.projects.cis.ksu.edu/

  11. JCAT: http://www.dai-arc.polito.it/dai-arc/auto/tools/tool6.shtml

  12. Java Model Checker: http://sprout.stanford.edu/uli/

  13. UV System: http://www.cs.utexas.edu/users/psp/markus/uv2/welcome.html

  14. Ptolemy II: http://ptolemy.eecs.berkeley.edu/ptolemyII/

  15. AutoFocus: http://autofocus.in.tum.de/index-e.html

  16. PVS: http://pvs.csl.sri.com

  17. ACL2: http://www.cs.utexas.edu/users/moore/acl2

  18. BLAST: http://www.cse.ucsd.edu/~rjhala/blast.html