Peer-Reviewed Publications

VMCAI 2020 screenshot

Jack Garzella, Marek Baranowski, Shaobo He, Zvonimir Rakamaric
Leveraging Compiler Intermediate Representation for Multi- and Cross-Language Verification
Proceedings of the 21st International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), 2020

TACO 2019 screenshot

Ian Briggs, Arnab Das, Marek Baranowski, Vishal Sharma, Sriram Krishnamoorthy, Zvonimir Rakamaric, Ganesh Gopalakrishnan
FailAmp: Relativization Transformation for Soft Error Detection in Structured Address Generation
ACM Transactions on Architecture and Code Optimimization (TACO), 2019

NSV 2019 screenshot

Shaobo He, Marek Baranowski, Zvonimir Rakamaric
Stochastic Local Search for Solving Floating-Point Constraints
Proceedings of the 12th International Workshop on Numerical Software Verification (NSV), 2019

NFM 2019 screenshot

Rocco Salvia, Laura Titolo, Marco A. Feliú, Mariano M. Moscato, César A. Muñoz, Zvonimir Rakamaric
A Mixed Real and Floating-Point Solver
Proceedings of the 11th NASA Formal Methods Symposium (NFM), 2019

MEMOCODE 2019 screenshot

Maryam Dabaghchian, Zvonimir Rakamaric
A Timeless Model for The Verification of Quasi-Periodic Distributed Systems
Proceedings of the 17th ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), 2019

IJHPCA 2019 screenshot

Kento Sato, Ignacio Laguna, Gregory L. Lee, Martin Schulz, Christopher M. Chambreau, Simone Atzeni, Michael Bentley, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Geof Sawaya, Joachim Protze, Dong H. Ahn
PRUNERS: Providing Reproducibility for Uncovering Non-Deterministic Errors in Runs on Supercomputers
International Journal of High Performance Computing Applications (IJHPCA), 2019

HotOS 2019 screenshot

Vikram Narayanan, Marek Baranowski, Leonid Ryzhyk, Zvonimir Rakamaric, Anton Burtsev
RedLeaf: Towards An Operating System for Safe and Verified Firmware
Proceedings of the 17th Workshop on Hot Topics in Operating Systems (HotOS), 2019

WAX 2018 screenshot

Rocco Salvia, Zvonimir Rakamaric
Exploring Floating-Point Trade-Offs in ML
Informal Proceedings of the Workshop on Approximate Computing Across the Stack (WAX), 2018

TOPLAS 2018 screenshot

Alexey Solovyev, Marek Baranowski, Ian Briggs, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan
Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
ACM Transactions on Programming Languages and Systems (TOPLAS), 2018

IPDPS 2018 screenshot

Simone Atzeni, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Ignacio Laguna, Gregory L. Lee, Dong H. Ahn
Sword: A Bounded Memory-Overhead Detector of OpenMP Data Races in Production Runs
Proceedings of the 32nd IEEE International Parallel and Distributed Processing Symposium (IPDPS), 2018

IFM 2018 screenshot

Marko Dimjasevic, Falk Howar, Kasper Luckow, Zvonimir Rakamaric
Study of Integrating Random and Symbolic Testing for Object-Oriented Software
Proceedings of the 14th International Conference on Integrated Formal Methods (IFM), 2018

ATVA 2018 screenshot

Marek Baranowski, Shaobo He, Zvonimir Rakamaric
Verifying Rust Programs with SMACK
Proceedings of the 16th International Symposium on Automated Technology for Verification and Analysis (ATVA), 2018

POPL 2017 screenshot

Wei-Fan Chiang, Marek Baranowski, Ian Briggs, Alexey Solovyev, Ganesh Gopalakrishnan, Zvonimir Rakamaric
Rigorous Floating-Point Mixed-Precision Tuning
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017

CRE 2017 screenshot

Kento Sato, Ignacio Laguna, Gregory L. Lee, Martin Schulz, Christopher M. Chambreau, Dong H. Ahn, Simone Atzeni, Michael Bentley, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Geof Sawaya, Joachim Protze
PRUNERS: Providing Reproducibility for Uncovering Non-Deterministic Errors in Runs on Supercomputers
Computational Reproducibility at Exascale Workshop (CRE), 2017

APLAS 2017 screenshot

Shaobo He, Zvonimir Rakamaric
Counterexample-Guided Bit-Precision Selection
Proceedings of the 15th Asian Symposium on Programming Languages and Systems (APLAS), 2017

TACAS 2016 screenshot

Kasper Luckow, Marko Dimjasevic, Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Temesghen Kahsai, Zvonimir Rakamaric, Vishwanath Raman
JDart: A Dynamic Symbolic Analysis Framework
Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2016

OOPSLA 2016 screenshot

Tyler Sorensen, Alastair F. Donaldson, Mark Batty, Ganesh Gopalakrishnan, Zvonimir Rakamaric
Portable Inter-workgroup Barrier Synchronisation for GPUs
Proceedings of the ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), 2016

NFM 2016 screenshot

Shaobo He, Shuvendu K. Lahiri, Zvonimir Rakamaric
Verifying Relative Safety, Accuracy, and Termination for Program Approximations
Proceedings of the 8th NASA Formal Methods Symposium (NFM), 2016

IPDPS 2016 screenshot

Simone Atzeni, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Dong H. Ahn, Ignacio Laguna, Martin Schulz, Gregory L. Lee, Joachim Protze, Matthias S. Muller
Archer: Effectively Spotting Data Races in Large OpenMP Applications
Proceedings of the 30th IEEE International Parallel and Distributed Processing Symposium (IPDPS), 2016

ICSE 2016 screenshot

Montgomery Carter, Shaobo He, Jonathan Whitaker, Zvonimir Rakamaric, Michael Emmi
SMACK Software Verification Toolchain
Proceedings of the 38th IEEE/ACM International Conference on Software Engineering (ICSE) Companion, 2016

TACAS 2015 screenshot

Arvind Haran, Montgomery Carter, Michael Emmi, Akash Lal, Shaz Qadeer, Zvonimir Rakamaric
SMACK+Corral: A Modular Verifier (Competition Contribution)
Proceedings of the 21st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2015

FM 2015 screenshot

Alexey Solovyev, Charles Jacobsen, Zvonimir Rakamaric, Ganesh Gopalakrishnan
Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions
Proceedings of the 20th International Symposium on Formal Methods (FM), 2015

ASE 2015 screenshot

Pantazis Deligiannis, Alastair F. Donaldson, Zvonimir Rakamaric
Fast and Precise Symbolic Analysis of Concurrency Bugs in Device Drivers
Proceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2015

PPoPP 2014 screenshot

Wei-Fan Chiang, Ganesh Gopalakrishnan, Zvonimir Rakamaric, Alexey Solovyev
Efficient Search for Inputs Causing High Floating-point Errors
Proceedings of the 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming (PPoPP), 2014

CiSE 2014 screenshot

Alan Humphrey, Qingyu Meng, Martin Berzins, Diego Caminha B. de Oliveira, Zvonimir Rakamaric, Ganesh Gopalakrishnan
Systematic Debugging Methods for Large Scale HPC Computational Frameworks
Computing in Science and Engineering (CiSE), 2014

CAV 2014 screenshot

Zvonimir Rakamaric, Michael Emmi
SMACK: Decoupling Source Language Details from Verifier Implementations
Proceedings of the 26th International Conference on Computer Aided Verification (CAV), 2014

2014_ASE_ghilrr screenshot

Dimitra Giannakopoulou, Falk Howar, Malte Isberner, Todd Lauderdale, Zvonimir Rakamaric, Vishwanath Raman
Taming Test Inputs for Separation Assurance
Proceedings of the 29th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2014

PRDC 2013 screenshot

Vishal Chandra Sharma, Arvind Haran, Zvonimir Rakamaric, Ganesh Gopalakrishnan
Towards Formal Approaches to System Resilience
Proceedings of the 19th IEEE Pacific Rim International Symposium on Dependable Computing (PRDC), 2013

NFM 2013 screenshot

Wei-Fan Chiang, Ganesh Gopalakrishnan, Guodong Li, Zvonimir Rakamaric
Formal Analysis of GPU Programs with Atomics via Conflict-Directed Delay-Bounding
Proceedings of the 5th NASA Formal Methods Symposium (NFM), 2013

2013_ISSTA_XPSYCO screenshot

Falk Howar, Dimitra Giannakopoulou, Zvonimir Rakamaric
Hybrid Learning: Interface Generation through Static, Dynamic, and Symbolic Analysis
Proceedings of the International Symposium on Software Testing and Analysis (ISSTA), 2013

2013_FORTE_FMOODS_br screenshot

Domagoj Babic, Zvonimir Rakamaric
Asynchronously Communicating Visibly Pushdown Systems
Proceedings of the 2013 IFIP Joint International Conference on Formal Techniques for Distributed Systems (33rd FORTE/15th FMOODS), 2013

SAS 2012 screenshot

Dimitra Giannakopoulou, Zvonimir Rakamaric, Vishwanath Raman
Symbolic Learning of Component Interfaces
Proceedings of the 19th International Static Analysis Symposium (SAS), 2012

BCHR_Fac screenshot

Domagoj Babic, Byron Cook, Alan J. Hu, Zvonimir Rakamaric
Proving Termination of Nonlinear Command Sequences
Formal Aspects of Computing (FAC), 2012

POPL 2011 screenshot

Michael Emmi, Shaz Qadeer, Zvonimir Rakamaric
Delay-Bounded Scheduling
Proceedings of the 38th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2011

ICSE 2010 screenshot

Zvonimir Rakamaric
STORM: Static Unit Checking of Concurrent Programs
Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering (ICSE) - Volume 2, 2010
 Silver Medal Winner in the ACM Student Research Competition

CLQR_STTT screenshot

Shaunak Chatterjee, Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric
A Low-Level Memory Model and an Accompanying Reachability Predicate
International Journal on Software Tools for Technology Transfer (STTT), 2009

CAV 2009 screenshot

Shuvendu Lahiri, Shaz Qadeer, Zvonimir Rakamaric
Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers
Proceedings of the 21st International Conference on Computer Aided Verification (CAV), 2009

2009_VMCAI_rh screenshot

Zvonimir Rakamaric, Alan J. Hu.
A Scalable Memory Model for Low-Level Code
Proceedings of the 10th International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 2009), 2009

2008_ASE_RH screenshot

Zvonimir Rakamaric, Alan J. Hu.
Automatic Inference of Frame Axioms Using Static Analysis
Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 2008

2007_SEFM_BCHR screenshot

Domagoj Babic, Byron Cook, Alan J. Hu., Zvonimir Rakamaric
Proving Termination by Divergence
Proceedings of the 5th IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007

2007_ATVA_RBHC screenshot

Zvonimir Rakamaric, Roberto Bruttomesso, Alan J. Hu., Alessandro Cimatti
Verifying Heap-Manipulating Programs in an SMT Framework
Proceedings of the 5th International Symposium on Automated Technology for Verification and Analysis (ATVA 2007), 2007

Other Publications