STeP
The Stanford Temporal Prover, STeP, is being developed by the REACT research group to support the computer-aided formal verification of reactive, real-time and hybrid systems based on their temporal specification. Unlike most systems for temporal verification, STeP is not restricted to finite-state systems, but combines model checking with deductive methods to allow the verification of a broad class of systems, including parameterized (N-component) circuit designs, parameterized (N-process) programs, and programs with infinite data domains.
Keywords for this software
References in zbMATH (referenced in 34 articles )
Showing results 1 to 20 of 34.
Sorted by year (- Fu, Jun; Wu, Jinzhao; Tan, Hongyan: A deductive approach towards reasoning about algebraic transition systems (2015)
- Schellhorn, Gerhard; Tofan, Bogdan; Ernst, Gidon; Pfähler, Jörg; Reif, Wolfgang: RGITL: a temporal logic framework for compositional reasoning about interleaved programs (2014)
- Hiraishi, Kunihiko; Kobayashi, Koich: An approximation algorithm for box abstraction of transition systems on real state spaces (2013)
- Platzer, André: Differential dynamic logic for hybrid systems (2008)
- Grumberg, Orna; Katz, Shmuel: VeriTech: a framework for translating among model description notations (2007) ioport
- Pretschner, Alexander; Prenninger, Wolfgang: Computing refactorings of state machines (2007) ioport
- Fang, Yi; McMillan, Kenneth L.; Pnueli, Amir; Zuck, Lenore D.: Liveness by invisible invariants (2006)
- Fang, Yi; Piterman, Nir; Pnueli, Amir; Zuck, Lenore: Liveness with invisible ranking (2006) ioport
- Kundaji, Rohit N.; Shyamasundar, R. K.: Refinement calculus: A basis for translation validation, debugging and certification (2006)
- Ţiplea, Ferucio Laurenţiu; Enea, Constantin: Abstractions of data types (2006)
- Kesten, Yonit; Piterman, Nir; Pnueli, Amir: Bridging the gap between fair simulation and trace inclusion (2005)
- Kesten, Yonit; Pnueli, Amir: A compositional approach to CTL(^*) verification (2005)
- Seow, Kiam Tian: Syntax-based synthesis for temporal-safety supervision (2005)
- Zuck, Lenore; Pnueli, Amir: Model checking and abstraction to the aid of parameterized systems (a survey) (2004)
- Armando, Alessandro; Ranise, Silvio: Constraint contextual rewriting. (2003)
- Armando, Alessandro; Rusinowitch, Michaël; Stratulat, Sorin: Incorporating decision procedures in implicit induction. (2002)
- Ölveczky, Peter Csaba; Meseguer, José: Specification of real-time and hybrid systems in rewriting logic (2002)
- Yu, Huiqun; He, Xudong; Deng, Yi; Mo, Lian: Formal analysis of real-time systems with SAM (2002)
- Bjørner, N. S.; Manna, Z.; Sipma, H. B.; Uribe, T. E.: Deductive verification of real-time systems using STeP (2001)
- Dietrich, F.; Logean, X.; Hubaux, J.-P.: Modeling and testing object-oriented distributed systems with linear-time temporal logic (2001)