scientific article; zbMATH DE number 1424030

zbMath0944.68040MaRDI QIDQ4945220

Jesper Møller, Jakob Lichtenberg, Henrik Hulgaard, Henrik Reif Andersen

Publication date: 23 March 2000

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

data structuredifference decision diagrams

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Data structures (68P05)

Related Items

Binary Decision Diagrams, Model Checking Real-Time Systems, A rewriting approach to binary decision diagrams, The octagon abstract domain, Model-Based Verification, Optimization, Synthesis and Performance Evaluation of Real-Time Systems, Efficient Evaluation of Arbitrary Relational Calculus Queries, Reachability analysis for timed automata using max-plus algebra, Formal verification based on Boolean expression diagrams, A Theoretical and Numerical Analysis of the Worst-Case Size of Reduced Ordered Binary Decision Diagrams, Unnamed Item, A symbolic model for timed concurrent constraint programming, Zero, successor and equality in BDDs, An Abstract Domain Extending Difference-Bound Matrices with Disequality Constraints, Improvements for the Symbolic Verification of Timed Automata, On the complexities of selected satisfiability and equivalence queries over Boolean formulas and inclusion queries over hulls, Symbolic model checking of timed guarded commands using difference decision diagrams

Uses Software

• Kronos
• Uppaal

Cites Work

• Symbolic model checking for real-time systems
• Kronos: A verification tool for real-time systems
• Uppaal in a nutshell
• Graph-Based Algorithms for Boolean Function Manipulation
• Unnamed Item
• Unnamed Item
• Unnamed Item