tlpvs: A pvs-Based ltl Verification System. In this paper we present our pvs implementation of a linear temporal logic verification system. The system includes a set of theories defining a temporal logic, a number of proof rules for proving soundness and response properties, and strategies which aid in conducting the proofs. In addition to implementing a framework for existing rules, we have also derived new methods which are particularly useful in a deductive ltl system. A distributed rank rule for the verification of response properties in parameterized systems is presented, and a methodology is detailed for reducing compassion requirements to justice requirements (strong fairness to weak fairness). Special attention has been paid to the verification of unbounded systems – systems in which the number of processes is unbounded – and our verification rules are appropriate to such systems.
Keywords for this software
References in zbMATH (referenced in 8 articles , 1 standard article )
Showing results 1 to 8 of 8.
- Bäumler, Simon; Schellhorn, Gerhard; Tofan, Bogdan; Reif, Wolfgang: Proving linearizability with temporal logic (2011)
- Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina: A model checking-based approach for security policy verification of mobile systems (2011)
- Cohen, Ariel; Pnueli, Amir; Zuck, Lenore D.: Mechanical verification of transactional memories with non-transactional memory accesses (2008)
- Hooman, Jozef; Kugler, Hillel; Ober, Iulian; Votintseva, Anjelika; Yushtein, Yuri: Supporting UML-based development of embedded systems by formal techniques (2008) ioport
- Cook, Byron; Kroening, Daniel; Sharygina, Natasha: Verification of Boolean programs with unbounded thread creation (2007)
- Hooman, Jozef; van der Zwaag, Mark B.: A semantics of communicating reactive objects with timing (2006) ioport
- Arons, Tamarah: Verification of an advanced Mips-type out-of-order execution algorithm (2004)
- Pnueli, Amir; Arons, Tamarah: tlpvs: A pvs-based ltl verification system (2003)