Papers by Radu Iosif

Iterating Octagons

Automata-based Termination Proofs

M. Bozga, P. Habermehl, R. Iosif, F. Konecny, and T. Vojnar. Automatic Verification of Integer Array Programs . Verimag Technical report number TR-2009-2.

R. Iosif. Symmetry Reductions for Model Checking of Concurrent Dynamic Software. Software Tools for Technology Transfer (STTT), Vol. 6, No. 4, 302 - 319, Springer-Verlag (2004).

R. Iosif, M. Dwyer, J. Hatcliff. Translating Java for Multiple Model Checkers: the Bandera Back End. Formal Methods in System Design (FSMD), Vol. 26, No. 2, Kluwer Academic Publishers (2005).

R. Iosif, R. Sisto. Temporal Logic Properties of Java Objects. Journal of Systems and Software, Elsevier Science Inc (2003).

C. Demartini, R. Iosif, R. Sisto. A Deadlock Detection Tool For Concurrent Java Programs. Software: Practice & Experience, Volume 29, Issue 7, (June 1999), 577 -- 603.

P. Habermehl, R. Iosif and T. Vojnar. A Logic of Singly Indexed Arrays. Proc. LPAR 2008 to appear.

M. Bozga, R. Iosif and S. Perarnau. Quantitative Separation Logic and Programs with Lists. Proc. IJCAR 2008, pp 34-49

P. Habermehl, R. Iosif and T. Vojnar. What else is decidable about integer arrays? Proc. FoSSaCS 2008, pp. 474-489

M. Bozga, R. Iosif and V. Sfyrla. An Efficient Algorithm for the Computation of Optimum Paths in Weighted Graphs. Workshop on Mathematical and Engineering Methods in Computer Science (MEMICS 2007).

Peter Habermehl, Radu Iosif, Adam Rogalewicz and Tomas Vojnar. Proving Termination of Tree Manipulating Programs. Intl. Symposium on Automated Technology for Verification and Analysis (ATVA 2007)

M. Bozga and R. Iosif. On Flat Programs with Lists. Proc. Intl.Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007). Lecture Notes in Computer Science, Vol. 4349, pp. 122-136. Extended version appeared as VERIMAG TR-2006-5.

2006
M. Bozga, R. Iosif and Y. Lakhnech. Flat Parametric Counter Automata. Proc. Intl. Conference on Automata, Languages and Programming (ICALP 2006).Lecture Notes in Computer Science Vol. 4052, pp 577-588. Extended version appeared as VERIMAG TR 2005-15.

A. Bouajjani, M. Bozga, P. Habermehl, R. Iosif, P. Moro and T. Vojnar. Programs with Lists are Counter Automata.Proc. Computer Aided Verification (CAV 2006). Lecture Notes in Computer Science Vol. 4144, pp 517-531. Extended version appeared as VERIMAG TR-2006-3.

P. Habermehl, R. Iosif and T. Vojnar. Automata-based Verification of Programs with Tree Updates Proc. 12th. International Conference on Tools and Algorithms for the Construction and the Analysis of Systems (TACAS 2006)

2005
M. Bozga and R. Iosif. Quantitative Verification of Programs with Lists. Proc.NATO Workshop on Verification of Infinite-state Systems with Applications to Security (VISSAS 2005)

M. Bozga and R. Iosif. On Decidability within the Arithmetic of Addition and Divisibility. Proc.Foundations of Software Science and Computation Structures (FOSSACS 2005), Lecture Notes in Computer Science Vol. 3441, pp 425 - 439

2004

M. Bozga, R. Iosif and Y. Lakhnech. On Logics of Aliasing.Proc. 11th Intl. Static Analysis Symposium (SAS04), Lecture Notes in Computer Science Vol. 3148, pp. 344 - 360, Springer Verlag (2004)

M. Bozga, R. Iosif. On Model Checking Generic Topologies.Proc. Workshop on Logics for Resources, Processes and Programs (LRPP04), pp. 73 - 87 (2004)

2003

Robby, M. B. Dwyer, J. Hatcliff, R. Iosif. Space-Reduction Strategies for Model Checking Dynamic Software.Proc. SoftMC03 Workshop on Software Model Checking, Electronic Notes in Theoretical Computer Science 89 No. 3 (2003)

M. Bozga, R. Iosif and Y. Lakhnech. Storeless Semantics and Alias Logic.Proc. ACM SIGPLAN 2003 Workshop on Partial Evaluation and Semantics Based Program Manipulation, ACM Press, pp 55 -- 65.

2002

R. Iosif. Symmetry Reduction Criteria for Software Model Checking.Proc. 9th SPIN Workshop on Software Model Checking, Lecture Notes in Computer Science, Volume 2318, Springer Verlag, pp 22 -- 41

2001

R. Iosif. Exploiting Heap Symmetries in Explicit-State Model Checking of Software.Proc 16th IEEE International Conference on Automated Software Engineering, pp. 254 -- 261 (November 2001)

2000

R. Iosif, R. Sisto.Using Garbage Collection in Model Checking.Proc. 7th SPIN Workshop, Lecture Notes in Computer Science, Volume 1885, pp. 20 -- 33, (September 2000).

R. Iosif. Formal Verification Applied to Java Concurrent Software.Proc. 22nd International Conference on Software Engineering (Doctoral Workshop), pp. 707 -- 709, (June 2000).

R. Iosif, R. Sisto. On the Specification and Semantics of Source Level Properties in Java.Proc. 1st International Workshop on Automated Program Analysis, Testing and Verification, pp. 83 -- 88 (June 2000)

1999 and earlier ...

C. Demartini, R. Iosif, R. Sisto. dSPIN: A Dynamic Extension of SPIN.Proc 6th SPIN Workshop. Lecture Notes in Computer Science, Volume 1680, pp. 261 -- 276, (September 1999).

C. Demartini, R. Iosif, R. Sisto.Modeling and Validation of Java Multi-threading Applications using SPIN.Proc. 4th SPIN Workshop. (November 1998) 5 -- 19.

C. Demartini, R. Iosif, R. Sisto. A Java-based Formal Development Environment for Factory Communication Systems.Proc 10th International IFIP wg 5.2/5.3 Conference PROLAMAT'98 (September 1998)

M. Bozga, R. Iosif. On Decidability within the Arithmetic of Addition and Divisibility. VERIMAG TR-2004-18.
M. Bozga, R. Iosif and Y. Lakhnech. On Logics of Aliasing. VERIMAG TR-2004-4.
M. Bozga, R. Iosif. On Model Checking Generic Topologies. VERIMAG TR-2004-7.
M. Bozga, R. Iosif Quantitative Verification of Programs with Lists.VERIMAG TR-2005-2.