swMATH8928MaRDI QIDQ20924FDOQ20924
Author name not available (Why is that?)
Official website: http://link.springer.com/chapter/10.1007/10722468_7
Cited In (95)
- Syntax-directed model checking of sequential programs
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Interpolation and model checking
- The word problem for visibly pushdown languages described by grammars
- Faster algorithms for weighted recursive state machines
- Program verification with interacting analysis plugins
- Verification, Model Checking, and Abstract Interpretation
- SAT-Based Model Checking
- Parameterised pushdown systems with non-atomic writes
- Title not available (Why is that?)
- On-the-Fly Techniques for Game-Based Software Model Checking
- Programming Languages and Systems
- Title not available (Why is that?)
- An Abort-Aware Model of Transactional Programming
- Types and trace effects of higher order programs
- Efficient SAT-based bounded model checking for software verification
- Visibly linear temporal logic
- Model-checking structured context-free languages
- Verification, Model Checking, and Abstract Interpretation
- A saturation method for the modal \(\mu \)-calculus over pushdown systems
- Formal analysis of hierarchical state machines
- PuMoC
- Title not available (Why is that?)
- Computer Aided Verification
- Summarization for termination: No return!
- First-Order and Temporal Logics for Nested Words
- Title not available (Why is that?)
- Alternating Automata and a Temporal Fixpoint Calculus for Visibly Pushdown Languages
- Verification of scope-dependent hierarchical state machines
- Predicate abstraction for program verification
- Model checking procedural programs
- A model checking-based approach for security policy verification of mobile systems
- Pushdown timed automata: A binary reachability characterization and safety verification.
- Model checking LTL with regular valuations for pushdown systems
- An automata-theoretic approach to infinite-state systems
- Context-aware counter abstraction
- Modular strategies for recursive game graphs
- Visibly rational expressions
- Counterexample-guided predicate abstraction of hybrid systems
- Hybrid automata-based CEGAR for rectangular hybrid systems
- Hybrid automata-based CEGAR for rectangular hybrid systems
- Application of static analyses for state-space reduction to the microcontroller binary code
- TopSpin
- Cogent
- Bogor
- bv2epr
- ComFoRT
- Title not available (Why is that?)
- Verification and falsification of programs with loops using predicate abstraction
- Bandera
- Java PathFinder
- CESAR
- dSPIN
- YASM
- MOPS
- d/dt
- TLPVS
- HARE
- SatAbs
- YOGI
- MAGIC
- Types and trace effects for object orientation
- Aglets
- DDVerify
- Moped
- EUREKA
- VPAlib
- OpenNWA
- WALi
- Compositional may-must program analysis: unleashing the power of alternation
- An Infinite Automaton Characterization of Double Exponential Time
- Programming Languages and Systems
- Model Checking Recursive Programs with Exact Predicate Abstraction
- Winning Regions of Pushdown Parity Games: A Saturation Method
- An abstract interpretation toolkit for \(\mu\)CRL
- CONCUR 2004 -- concurrency theory. 15th international conference, London, UK, August 31 -- September 3, 2004. Proceedings.
- Tools and Algorithms for the Construction and Analysis of Systems
- Bisimulation conversion and verification procedure for goal-based control systems
- Hybrid Systems: Computation and Control
- Verification of Boolean programs with unbounded thread creation
- CPBPV: a constraint-programming framework for bounded program verification
- Title not available (Why is that?)
- Tools and Algorithms for the Construction and Analysis of Systems
- Reducing concurrent analysis under a context bound to sequential analysis
- Visibly pushdown languages
- Title not available (Why is that?)
- Interprocedural Analysis of Concurrent Programs Under a Context Bound
- Model Checking Software
- Analyzing pushdown systems with stack manipulation
- Title not available (Why is that?)
- SMT-based model checking for recursive programs
- Translating Java for multiple model checkers: The Bandera back-end
- Verifying time partitioning in the DEOS scheduling kernel
- Title not available (Why is that?)
This page was built for software: Bebop
