scientific article
From MaRDI portal
Publication:2753756
zbMath0976.68540MaRDI QIDQ2753756
Thomas Ball, Sriram K. Rajamani
Publication date: 11 November 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Computing methodologies and applications (68U99) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (49)
Ramsey-Based Inclusion Checking for Visibly Pushdown Automata ⋮ Model-checking structured context-free languages ⋮ Modular strategies for recursive game graphs ⋮ Counterexample-guided predicate abstraction of hybrid systems ⋮ Model checking LTL with regular valuations for pushdown systems ⋮ SAT-Based Model Checking ⋮ Abstraction and Abstraction Refinement ⋮ Interpolation and Model Checking ⋮ Predicate Abstraction for Program Verification ⋮ Model Checking Procedural Programs ⋮ Summarization for termination: No return! ⋮ Winning Regions of Pushdown Parity Games: A Saturation Method ⋮ Program verification with interacting analysis plugins ⋮ Context-aware counter abstraction ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ An abstract interpretation toolkit for \(\mu\)CRL ⋮ Hybrid automata-based CEGAR for rectangular hybrid systems ⋮ Verification of programs with exceptions through operator precedence automata ⋮ Application of static analyses for state-space reduction to the microcontroller binary code ⋮ Pushdown timed automata: A binary reachability characterization and safety verification. ⋮ Complete SAT-Based Model Checking for Context-Free Processes ⋮ Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis ⋮ Bisimulation conversion and verification procedure for goal-based control systems ⋮ A model checking-based approach for security policy verification of mobile systems ⋮ Analyzing pushdown systems with stack manipulation ⋮ Splitting the Control Flow with Boolean Flags ⋮ Faster Algorithms for Weighted Recursive State Machines ⋮ Model Checking Recursive Programs with Exact Predicate Abstraction ⋮ An Infinite Automaton Characterization of Double Exponential Time ⋮ Visibly rational expressions ⋮ The word problem for visibly pushdown languages described by grammars ⋮ Verification of Boolean programs with unbounded thread creation ⋮ Efficient SAT-based bounded model checking for software verification ⋮ Verification of scope-dependent hierarchical state machines ⋮ Visibly linear temporal logic ⋮ SMT-based model checking for recursive programs ⋮ A saturation method for the modal \(\mu \)-calculus over pushdown systems ⋮ Verification and falsification of programs with loops using predicate abstraction ⋮ CPBPV: a constraint-programming framework for bounded program verification ⋮ An Automata-Theoretic Approach to Infinite-State Systems ⋮ Unnamed Item ⋮ On-the-Fly Techniques for Game-Based Software Model Checking ⋮ Program Analysis Using Weighted Pushdown Systems ⋮ Types and trace effects for object orientation ⋮ Unnamed Item ⋮ Reducing concurrent analysis under a context bound to sequential analysis ⋮ Syntax-directed model checking of sequential programs ⋮ Verifying time partitioning in the DEOS scheduling kernel ⋮ Translating Java for multiple model checkers: The Bandera back-end
Uses Software
This page was built for publication:
