Valigator: A Verification Tool with Bound and Invariant Generation

DOI10.1007/978-3-540-89439-1_24MaRDI QIDQ5505564zbMATH OpenOpenAlexFDO

Authors Thibaud Hottelier, Laura Kovács, Thomas A. Henzinger

Publication date 27 January 2009

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-89439-1_24

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Symbolic computation and algebraic computation (68W30)

Recommendations

• Computer Aided Verification
• Model Checking Software
• Synthesizing invariants by solving solvable loops
• Theoretical Aspects of Computing - ICTAC 2004
• Aligator: A Mathematica Package for Invariant Generation (System Description)

Cited in

(6)

• Valigator
• Lingva: generating and proving program properties using symbol elimination
• scientific article; zbMATH DE number 1903374 (Why is no real title available?)
• Computing exact loop bounds for bounded program verification
• Model Checking Software
• Computer Aided Verification

Describes a project that uses

Uses Software

• SPARK
• PVS
• JML
• z3
• Scala
• ESC/Java
• KeY
• Spec#
• SIMPLIFY
• Boogie
• LOOP

This page was built for publication: Valigator: A Verification Tool with Bound and Invariant Generation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5505564)