Certificate-Based Verification and Synthesis: Tools and Benchmarks
Tools
These are some freely available tools that enable
certificate-based verification by providing
quantifier elimination and simplification capabilities.
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.
Publications
Main publication explaining the benchmarks and the use of
the tools on the benchmarks:
Thomas Sturm and Ashish Tiwari,
"Verification and Synthesis Using Real Quantifier Elimination".
Other publications based on the concept of
Certificate-Based Verification and Synthesis
- 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.
- 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.
- Ashish Tiwari,
"Generating Box Invariants", In HSCC 2008.
-
E. Rodriguez-Carbonell and Ashish Tiwari,
"Generating Polynomial Invariants for Hybrid Systems",
In Hybrid Systems: Computation and Control 2005.
-
Gaurav Khanna and Ashish Tiwari,
"
Nonlinear Systems: Approximating Reach Sets ",
In HSCC 2004.
-
Ashish Tiwari,
"Approximate Reachability for Linear Systems",
In the Proceedings of Hybrid Systems: Computation and Control,
HSCC 2003.
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
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