ACI Dynamo

Goal: Verification of Dynamic Embedded Programs.

Click here for a detailed description in French.

Partners

Meetings

 Grenoble, 28 Nov 2003
 Grenoble, 27 May 2004
 Paris, 1 March 2005
 Paris, 28 November 2005
 Grenoble, 26 June 2006

Workshops

 HEAP Workshop, 28 May 2004, Grenoble
 COSMICAH 2005 (Lisbon 10 July, ICALP 2005 satellite workshop)

Publications

[1] Marius Bozga, Radu Iosif, and Yassine Lakhnech. Counting aliases. Technical Report 17, Verimag, October 2004.
[ bib ]
[2] Marius Bozga, Radu Iosif, and Yassine Lakhnech. Storeless semantics and alias logic. In Proc. ACM SIGPLAN 2003 Workshop on Partial Evaluation and Semantics Based Program Manipulation, pages 55 - 65. ACM Press, 2003.
[ bib ]
[3] Marius Bozga and Radu Iosif. On model checking generic topologies. In Proc. LICS-ICALP Workshop on Logics for Resources, Processes and Programs (LRPP04), pages 73 - 87, 2004.
[ bib ]
[4] Marius Bozga, Radu Iosif, and Yassine Lakhnech. On logics of aliasing. In Proc. 11th Intl. Static Analysis Symposium (SAS04), pages 344 - 360. Springer-Verlag, 2004.
[ bib ]
[5] Marius Bozga and Radu Iosif. On decidability with the arithmetic with addition and divisibility. In Proc. Foundations of Software Science and Computation Structures (FOSSACS 2005), pages 425 - 439. Springer-Verlag, 2005.
[ bib ]
[6] Marius Bozga and Radu Iosif. Quantitative verification of programs with lists. In Proc. NATO Workshop on Verification of Infinite-state Systems with Applications to Security (VISSAS 2005), 2005.
[ bib ]
[7] G. Salagnac, S. Yovine, and D. Garbervetsky. Fast escape analysis for region-based memory management. In Proceedings of Abstract Interpretation for Object-Oriented Languages, AIOOL'05. To appear in ENTCS, Elsevier, 2005.
[ bib ]
[8] D. Garbervetsky, C. Nakhli, S. Yovine, and H. Zorgati. Program instrumentation and run-time analysis of scoped memory in java. In Workshop on Runtime Verification, RV'04. ENTCS 113, Elsevier, 2005.
[ bib ]
[9] V. Braberman, D. Garbervetsky, and S. Yovine. Synthesizing parametric specifications of dynamic memory utilization in imperative object oriented programs. Technical Report, submitted for publication, 2005.
[ bib ]
[10] A. Bouajjani, P. Habermehl, and T. Vojnar. Abstract Regular Model Checking. In Proceedings of CAV'04, volume 3114 of LNCS. Springer, 2004.
[ bib ]
[11] P. Habermehl and T. Vojnar. Regular Model Checking Using Inference of Regular Languages. In Proceedings of the 6th Infinity Workshop. to appear in ENTCS, 2004.
[ bib ]
[12] Ahmed Bouajjani and Tayssir Touili. On Computing Reachability Sets of Process Rewrite Systems. In RTA'05. LNCS, 2005.
[ bib ]
[13] A. Bouajjani, J. Esparza, and T. Touili. Reachability Analysis of Synchronised PA systems. In Proceedings of the 6th Infinity Workshop. to appear in ENTCS, 2004.
[ bib ]
[14] T. Touili. Dealing with communication for dynamic multithreaded recursive programs. In 1st VISSAS workshop, 2005. Invited Paper.
[ bib ]
[15] A. Bouajjani, P. Habermehl, P. Moro, and T. Vojnar. Verifying programs with 1-selector-linked structures in regular model checking. In TACAS, volume 3440 of LNCS. Springer, 2005.
[ bib ]
[16] A. Bouajjani and A. Meyer. Symbolic reachability analysis of higher-order context-free processes. In Proceedings of the 24th Intern. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS'04), volume 3328 of LNCS. Springer, 2004.
[ bib ]
[17] A. Bouajjani, A. Legay, and P. Wolper. Handling liveness properties in (omega-)regular model checking. In Proceedings of the 6th Intern. Workshop on Verification of Infinite-State Systems (Infinity'04). to appear in ENTCS, 2004.
[ bib ]

This file has been generated by bibtex2html 1.75