Bebop

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