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.

References in zbMATH (referenced in 36 articles )

Showing results 1 to 20 of 36.
Sorted by year (citations)

1 2 next

  1. Fu, Jun; Wu, Jinzhao; Tan, Hongyan: A deductive approach towards reasoning about algebraic transition systems (2015)
  2. Schellhorn, Gerhard; Tofan, Bogdan; Ernst, Gidon; Pfähler, Jörg; Reif, Wolfgang: RGITL: a temporal logic framework for compositional reasoning about interleaved programs (2014)
  3. Hiraishi, Kunihiko; Kobayashi, Koich: An approximation algorithm for box abstraction of transition systems on real state spaces (2013)
  4. Platzer, André: Differential dynamic logic for hybrid systems (2008)
  5. Grumberg, Orna; Katz, Shmuel: VeriTech: a framework for translating among model description notations (2007) ioport
  6. Pretschner, Alexander; Prenninger, Wolfgang: Computing refactorings of state machines (2007) ioport
  7. Fang, Yi; McMillan, Kenneth L.; Pnueli, Amir; Zuck, Lenore D.: Liveness by invisible invariants (2006)
  8. Fang, Yi; Piterman, Nir; Pnueli, Amir; Zuck, Lenore: Liveness with invisible ranking (2006) ioport
  9. Kundaji, Rohit N.; Shyamasundar, R. K.: Refinement calculus: A basis for translation validation, debugging and certification (2006)
  10. Ţiplea, Ferucio Laurenţiu; Enea, Constantin: Abstractions of data types (2006)
  11. Kesten, Yonit; Piterman, Nir; Pnueli, Amir: Bridging the gap between fair simulation and trace inclusion (2005)
  12. Kesten, Yonit; Pnueli, Amir: A compositional approach to CTL(^*) verification (2005)
  13. Seow, Kiam Tian: Syntax-based synthesis for temporal-safety supervision (2005)
  14. Zuck, Lenore; Pnueli, Amir: Model checking and abstraction to the aid of parameterized systems (a survey) (2004)
  15. Armando, Alessandro; Ranise, Silvio: Constraint contextual rewriting. (2003)
  16. Sen, Koushik; Roşu, Grigore; Agha, Gul: Generating optimal linear temporal logic monitors by coinduction. (2003)
  17. Armando, Alessandro; Rusinowitch, Michaël; Stratulat, Sorin: Incorporating decision procedures in implicit induction. (2002)
  18. Ölveczky, Peter Csaba; Meseguer, José: Specification of real-time and hybrid systems in rewriting logic (2002)
  19. Yu, Huiqun; He, Xudong; Deng, Yi; Mo, Lian: Formal analysis of real-time systems with SAM (2002)
  20. Bjørner, N. S.; Manna, Z.; Sipma, H. B.; Uribe, T. E.: Deductive verification of real-time systems using STeP (2001)

1 2 next