Certificate-Based Verification and Synthesis: Tools and Benchmarks
Tools
Listed below are some freely available tools that enable
certificate-based verification by providing
quantifier elimination and/or simplification capabilities
on nonlinear formulas.
Reduce/Redlog can now call qepcad for performing quantifier elimination.
Exists-Forall Benchmarks
Certificates for verification and synthesis can be generated
by solving exists-forall formulas. Here are some exists-forall
benchmarks thus generated. They are provided as reduce/redlog input files.
Exists Benchmarks
Generated by HybridSal relational abstracter and SAL infinite bounded model checker
HybridSal relational abstraction tool can be downloaded from
here.
Publications
Publications on Certificate-Based Verification and Synthesis
-
Thomas Sturm and Ashish Tiwari,
"Verification and Synthesis Using Real Quantifier Elimination". In ISSAC 2011.
- Ankur Taly and Sumit Gulwani and Ashish Tiwari,
"Synthesizing switching logic using constraint solving",
In Intl. journal on software tools for technology transfer (STTT).
SpringerLink.
- Ashish Tiwari,
"Compositionally analyzing a PI controller formally", In Proc. IEEE Conf. on Decision and Control,
CDC 2011.
- Ankur Taly and Ashish Tiwari,
"Switching logic synthesis for reachability",
In EMSOFT 2010.
- Ashish Tiwari,
"Bounded verification of adaptive flight control systems",
Proc. AIAA Infotech@Aerospace, 2010. AIAA-2010-3362.
- Ankur Taly and Ashish Tiwari,
"Deductive Verification of Continuous Dynamical Systems",
In FSTTCS'09.
- Ashish Tiwari,
"Formally analyzing adaptive flight control."
In NSV II (co-located with CPSWeek 2009).
- Ankur Taly and Ashish Tiwari,
Sumit Gulwani,
"Synthesizing Switching Logic using Constraint Solving."
In VMCAI 2009.
-
Sumit Gulwani
and Ashish Tiwari,
"Constraint-based Approach for Verification and Synthesis of Hybrid Systems",
CAV 2008.
- Aditya Zutshi, Sriram Sankaranarayanan, and Ashish Tiwari,
"Timed Relational Abstractions For Sampled Data Control Systems".
, In CAV 2012.
- Ashish Tiwari,
"HybridSal Relational Abstracter".
In CAV 2012.
- Sergio Mover, Alessandro Cimatti, Ashish Tiwari and Stefano Tonetta,
"Time-aware relational abstraction for Hybrid systems", In EMSOFT 2013.
-
Older relevant papers:
Papers by other groups on certificate-based verification:
- Barrier certificates (Prajna, Parrillo and others)
- Template-based approaches (Sankaranarayanan and others)
- Lyapunov function and its region-of-attraction (Packard and others)
-
Template-based verification
Talks/Lectures
-
Bruno Dutertre gave lectures on SMT solving and applications
at the following events.
- "Summer School in Formal Techniques" held at Menlo College, Atherton, CA, May 22-27, 2011.
- "SAT/SMT Solver Summer School 2011" held at MIT, Cambridge MA, June 12-17, 2011.
- Second International SAT/SMT Summer School held at Trento, Italy, June 12-15, 2012.
- Second Summer School on Formal Techniques held at Menlo College, Atherton, CA, May 27-June 1, 2012.
- Talks by Ashish:
- Invited talk at
LICS 2011,
Fields Institute, Toronto, Jun 21, 2011.
- Invited talk at
RTA 2011,
Novi Sad, Serbia, May 31, 2011.
- Invited talk at
ISSAC 2011,
Munich, July 26, 2010.
Acknowledgments
This material is based upon work supported in part
by the National Science Foundation under
Grant No. 0917398
and
Grant No. 1017483.
Any opinions, findings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the National Science Foundation.
This page is maintained by Ashish Tiwari.
Return to the Formal Methods Program home page
Return to the Computer Science Laboratory home page