VIS

VIS (Verification Interacting with Synthesis) is a system for formal verification, synthesis, and simulation of finite state systems. It has been developed jointly at the University of California at Berkeley, the University of Colorado at Boulder, and more recently at the University of Texas, Austin. Verification is the process of checking if ”what was designed is what was originally specified”. While the traditional and most common method of verification is through simulation, recently, interest has increased in methods of formal verification, such as language containment and temporal logic model checking. VIS is able to synthesize finite state systems and/or verify properties of such systems, which have been specified hierarchically as a collection of interacting finite state machines.


References in zbMATH (referenced in 17 articles )

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

  1. Cimatti, Alessandro; Roveri, Marco; Tonetta, Stefano: HRELTL: a temporal logic for hybrid systems (2015)
  2. Ray, Sandip; Sumners, Rob: Specification and verification of concurrent programs through refinements (2013)
  3. Jobstmann, Barbara; Staber, Stefan; Griesmayer, Andreas; Bloem, Roderick: Finding and fixing faults (2012)
  4. Cabodi, Gianpiero; Nocco, Sergio; Quer, Stefano: Benchmarking a model checker for algorithmic improvements and tuning for performance (2011)
  5. Li, Yongjian; Hung, William N. N.; Song, Xiaoyu; Zeng, Naiju: Exploring structural symmetry automatically in symbolic trajectory evaluation (2011)
  6. Rozier, Kristin Y.: Linear temporal logic symbolic model checking (2011)
  7. Beaudenon, Vincent; Encrenaz, Emmanuelle; Taktak, Sami: Data decision diagrams for Promela systems analysis (2010) ioport
  8. Rozier, Kristin Y.; Vardi, Moshe Y.: LTL satisfiability checking (2010) ioport
  9. Vardi, Moshe Y.: From philosophical to industrial logics (2009)
  10. Gentilini, Raffaella; Piazza, Carla; Policriti, Alberto: Symbolic graphs: Linear solutions to connectivity related problems (2008)
  11. Tronci, Enrico: Introductory paper (2006) ioport
  12. Wang, Chao; Bloem, Roderick; Hachtel, Gary D.; Ravi, Kavita; Somenzi, Fabio: Compositional SCC analysis for language emptiness (2006)
  13. Li, Bing; Wang, Chao; Somenzi, Fabio: Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure (2005) ioport
  14. Li, Bing; Wang, Chao; Somenzi, Fabio: Abstraction refinement in symbolic model checking using satisfiability as the only decision procedure (2005) ioport
  15. Staber, Stefan; Jobstmann, Barbara; Bloem, Roderick: Finding and fixing faults (2005)
  16. Jin, Hoonsang; Ravi, Kavita; Somenzi, Fabio: Fate and free will in error traces (2004) ioport
  17. Katoen, Joost-Pieter; Stevens, Perdita: Guest editors’ introduction: advancements and extensions of verification techniques (2004) ioport