Curso Dr. Ahmed Bouajjani

Algorithmic Techniques for Program Verification

 

Abstract 

The design of automatic program verification techniques is highly challeng- ing both from the theoretical and practical point of view. The sources of complexity are multiple, concerning aspects related to (1) the used control primitives such as procedure calls, recursion, concurrency, dynamic creations of tasks, etc., as well as aspects related to (2) the dependency from data over infinite domains and the manipulation of (dynamic) data structures. The design of formal program verification methods requires the development of techniques allowing to handle infinite-state models (due the unboundedness of both control and data structures) that are beyond the capabilities of the standard finite-state model-checking algorithms. The aim of this course is to present a broad view on the existing algorithmic verification techniques for various classes of programs, including sequential programs with recursive procedure calls, concurrent programs with dynamic creation of tasks, and programs manipulating infinite data and unbounded data structures.

Content 

The course is composed of the five following lectures:

  1. Programs with procedure calls Recursive state machines. Pushdown systems (PDS). Proce- dure summarization. Automata-based reachability analysis. Model-checking. [BEM97, ABE+05, ABE12].  
  2. Concurrent programs with dynamic creation of tasks (Part 1) Petri nets/Vector addition systems. State reachability, coverability. Communicating pushdown systems. Constrained dynamic networks of pushdown systems. [BMOT05, BE06].
  3. Concurrent programs with dynamic creation of tasks (Part 2) Asynchronous programs. (Recursively Parallel Programs.) Context-bounded analysis. Sequentialization. [SV06, LR09, LMP10, BEP11, BE12]
  4. Programs with integer data Abstraction, acceleration techniques, (pattern-based invari- ant synthesis). [GS97, McM05, WB98, BIL06, SSM04] 
  5. Programs with dynamic linked lists/unbounded arrays Decidable logics for pre-post-condition reasoning: Small model property, automata-based approach [BDES09, HIV08]

References

[ABE+ 05]

Rajeev Alur, Michael Benedikt, Kousha Etessami, Patrice Gode- froid, Thomas W. Reps, and Mihalis Yannakakis. Analysis of recursive state machines. ACM Trans. Program. Lang. Syst., 27(4):786–818, 2005.

[ABE12]

Rajeev Alur, Ahmed Bouajjani, and Javier Esparza. Model- checking of procedural programs. Handbook of Model-Checking, 2012. to appear.

[BDES09]

Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, and Mi- haela Sighireanu. A logic-based framework for reasoning about composite data structures. In CONCUR, volume 5710 of Lecture Notes in Computer Science, pages 178–195. Springer, 2009.

[BE06]

Ahmed Bouajjani and Javier Esparza. Rewriting models of boolean programs. In RTA ’06: Proc. 17th International Con- ference on Term Rewriting and Applications, volume 4098 of LNCS, pages 136–150. Springer, 2006.

[BE12] 

Ahmed Bouajjani and Michael Emmi. Analysis of recursively parallel programs. In POPL, January 2012. to appear.

[BEM97]

Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reacha- bility analysis of pushdown automata: Application to model- checking. In CONCUR, volume 1243 of Lecture Notes in Com- puter Science, pages 135–150. Springer, 1997.

[BEP11]

Ahmed Bouajjani, Michael Emmi, and Gennaro Parlato. On sequentializing concurrent programs. In SAS ’11: Proc. 18th Int. Symp. on Static Analysis. Springer, 2011.

[BIL06]

Marius Bozga, Radu Iosif, and Yassine Lakhnech. Flat paramet- ric counter automata. In ICALP (2), volume 4052 of Lecture Notes in Computer Science, pages 577–588. Springer, 2006.

[BMOT05]

Ahmed Bouajjani, Markus Muller-Olm, and Tayssir Touili. Regular symbolic analysis of dynamic networks of pushdown sys- tems. In CONCUR ’05: Proc. 16th International Conference on Concurrency Theory, volume 3653 of LNCS, pages 473–487. Springer, 2005.

[GS97]

Susanne Graf and Hassen Saidi. Construction of abstract state graphs with pvs. In CAV, volume 1254 of Lecture Notes in Computer Science, pages 72–83. Springer, 1997.

[HIV08]

Peter Habermehl, Radu Iosif, and Tom ́as Vojnar. What else is decidable about integer arrays? In FoSSaCS, volume 4962 of Lecture Notes in Computer Science, pages 474–489. Springer, 2008.

[LMP10]

Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Model-checking parameterized concurrent programs using lin- ear interfaces. In CAV ’10: Proc. 22nd International Conference on Computer Aided Verification, volume 6174 of LNCS, pages 629–644. Springer, 2010.

[LR09]

Akash Lal and Thomas W. Reps. Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design, 35(1):73–97, 2009.

[McM05]

Kenneth L. McMillan. Applications of craig interpolants in model checking. In TACAS, volume 3440 of Lecture Notes in Computer Science, pages 1–12. Springer, 2005.

[SSM04]

Sriram Sankaranarayanan, Henny B. Sipma, and Zohar Manna. Constraint-based linear-relations analysis. In SAS, volume 3148 of Lecture Notes in Computer Science, pages 53–68. Springer, 2004.

[SV06]

Koushik Sen and Mahesh Viswanathan. Model checking multi- threaded programs with asynchronous atomic methods. In CAV ’06: Proc. 18th International Conference on Computer Aided Verification, volume 4144 of LNCS, pages 300–314. Springer, 2006.

[WB98]

Pierre Wolper and Bernard Boigelot. Verifying systems with infinite but regular state spaces. In CAV, volume 1427 of Lecture Notes in Computer Science, pages 88–97. Springer, 1998.