SMACK+ Corral: A Modular Verifier: (Competition Contribution)
Tools and Algorithms for the Construction and Analysis of Systems: 21st …, 2015•Springer
LNCS 9035 - SMACK+Corral: A Modular Verifier Page 1 SMACK+Corral: A Modular Verifier
⋆ (Competition Contribution) Arvind Haran 1 , Montgomery Carter 1 , Michael Emmi 2 ,
Akash Lal 3 , Shaz Qadeer 3 , and Zvonimir Rakamaric 1 1 School of Computing, University
of Utah, USA zvonimir@cs.utah.edu 2 IMDEA Software Institute, Spain michael.emmi@imdea.org
3 Microsoft Research, India & USA akashl@microsoft.com Abstract. SMACK and Corral are
two components of a modular toolchain for verifying C programs. Together they exploit state-of-the-art …
⋆ (Competition Contribution) Arvind Haran 1 , Montgomery Carter 1 , Michael Emmi 2 ,
Akash Lal 3 , Shaz Qadeer 3 , and Zvonimir Rakamaric 1 1 School of Computing, University
of Utah, USA zvonimir@cs.utah.edu 2 IMDEA Software Institute, Spain michael.emmi@imdea.org
3 Microsoft Research, India & USA akashl@microsoft.com Abstract. SMACK and Corral are
two components of a modular toolchain for verifying C programs. Together they exploit state-of-the-art …
Abstract
SMACK and Corral are two components of a modular toolchain for verifying C programs. Together they exploit state-of-the-art compiler technologies and theorem provers to simplify and dispatch verification conditions.
Springer
