Cadence SMV

Cadence SMV is a symbolic model checking tool that allows you to formally verify temporal logic properties of finite state systems, such as computer hardware designs. That means that instead of writing a simulation vectors or a simulation test bench, you verify your design for all possible input sequences. While formal verification is often equated with equivalence checking, model checking is substantially more general. It allows you to verify that that your specifications are correct very early in the design process by building abstract system level models. Its use continues through the design refinement process, allowing you to verify that your RTL level design correctly implements your high level model.

References in zbMATH (referenced in 27 articles )

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

1 2 next

  1. Li, Jianwen; Zhang, Lijun; Zhu, Shufang; Pu, Geguang; Vardi, Moshe Y.; He, Jifeng: An explicit transition system construction approach to LTL satisfiability checking (2018)
  2. Dietsch, Daniel; Heizmann, Matthias; Langenfeld, Vincent; Podelski, Andreas: Fairness modulo theory: a new approach to LTL software model checking (2015)
  3. Koo, T. John; Li, Rongqing; Quottrup, Michael M.; Clifton, Charles A.; Izadi-Zamanabadi, Roozbeh; Bak, Thomas: A framework for multi-robot motion planning from temporal logic specifications (2012)
  4. Rozier, Kristin Y.: Linear temporal logic symbolic model checking (2011)
  5. Chen, Mingsong; Mishra, Prabhat; Kalita, Dhrubajyoti: Efficient test case generation for validation of UML activity diagrams (2010) ioport
  6. Rozier, Kristin Y.; Vardi, Moshe Y.: LTL satisfiability checking (2010) ioport
  7. Calder, M.; Miller, A.: An automatic abstraction technique for verifying featured, parameterised systems (2008)
  8. Clarke, Edmund; Talupur, Murali; Veith, Helmut: Proving Ptolemy right: The environment abstraction framework for model checking concurrent systems (2008)
  9. Ferrante, Alessandro; Napoli, Margherita; Parente, Mimmo: CTL model-checking with graded quantifiers (2008)
  10. Gupta, Anubhav; McMillan, K. L.; Fu, Zhaohui: Automated assumption generation for compositional verification (2008)
  11. Feng, L.; Wonham, W. M.; Thiagarajan, P. S.: Designing communicating transaction processes by supervisory control theory (2007)
  12. Klai, Kais; Petrucci, Laure; Reniers, Michel: An incremental and modular technique for checking LTL(\setminus)X properties of Petri nets (2007)
  13. Loer, Karsten; Harrison, Michael D.: An integrated framework for the analysis of dependable interactive systems (IFADIS): its tool support and evaluation (2006) ioport
  14. Pan, Hong; Lin, Hui-Min; Lv, Yi: Model checking data consistency for cache coherence protocols (2006) ioport
  15. Tverdyshev, Sergey: Combination of Isabelle/HOL with automatic tools (2005)
  16. Barbuti, Roberto; Bernardeschi, Cinzia; de Francesco, Nicoletta: Analyzing information flow properties in assembly code by abstract interpretation (2004)
  17. Chou, Ching-Tsun; Mannava, Phanindra K.; Park, Seungjoon: A simple method for parameterized verification of cache coherence protocols (2004)
  18. Lahiri, Shuvendu K.; Bryant, Randal E.: Indexed predicate discovery for unbounded system verification (2004)
  19. Win, Toh Ne; Ernst, Michael D.; Garland, Stephen J.; Kırlı, Dilsun; Lynch, Nancy A.: Using simulated execution in verifying distributed algorithms (2004) ioport
  20. Zuck, Lenore; Pnueli, Amir: Model checking and abstraction to the aid of parameterized systems (a survey) (2004)

1 2 next