Verifying Heap-Manipulating Programs in an SMT Framework
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti. 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), Tokyo, Japan.
Category Archives: Publications
Proving Termination by Divergence
Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric. 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), London, UK.
Deciding Unbounded Heaps in an SMT Framework
Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu, Alessandro Cimatti. 5th International Workshop on Satisfiability Modulo Theories (SMT 2007), Berlin, Germany. (Presentation-only paper.)
A Reachability Predicate for Analyzing Low-Level Software
Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric. 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2007), Braga, Portugal. Outstanding Student Paper Award. Invited for special section submission…
An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures
Zvonimir Rakamaric, Jesse Bingham, Alan J. Hu. 8th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2007), Nice, France.
A Reachability Predicate for Analyzing Low-Level Software
Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric. Microsoft Research Tech Report MSR-TR-2006-154, November, 2006.
A Logic and Decision Procedure for Verification of Heap-Manipulating Programs
Zvonimir Rakamaric. M.Sc. Thesis, Department of Computer Science, The University of British Columbia, August, 2006.
A Better Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs
Zvonimir Rakamaric, Jesse Bingham, Alan J. Hu. UBC Department of Computer Science Tech Report TR-2006-02, January 30, 2006.
A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs
Jesse Bingham, Zvonimir Rakamaric. 7th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2006), Charleston, SC, USA.
A Logic and Decision Procedure for Predicate Abstraction of Heap-Manipulating Programs
Jesse Bingham, Zvonimir Rakamaric. UBC Department of Computer Science Tech Report TR-2005-19, September 19, 2005.