TACAS 2007
56 papers
- "Don't Care" Modeling: A Logical Framework for Developing Predictive System Models
- A Generic Framework for Reasoning About Dynamic Networks of Infinite-State Processes
- A Gröbner Basis Approach to CNF-Formulae Preprocessing
- A Reachability Predicate for Analyzing Low-Level Software
- A Symbolic Algorithm for Optimal Markov Chain Lumping
- Abstraction Refinement of Linear Programs with Arrays
- Adaptor Synthesis for Real-Time Components
- Alloy Analyzer+PVS in the Analysis and Verification of Alloy Specifications
- Assume-Guarantee Synthesis
- Automatic Analysis of the Security of XOR-Based Key Management Schemes
- Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking
- Bounded Reachability Checking of Asynchronous Systems Using Decision Diagrams
- Causal Dataflow Analysis for Concurrent Programs
- Checking Pedigree Consistency with PCS
- Combined Satisfiability Modulo Parametric Theories
- Combining Abstraction Refinement and SAT-Based Model Checking
- Complexity in Simplicity: Flexible Agent-Based State Space Exploration
- Counterexamples in Probabilistic Model Checking
- Deciding Bit-Vector Arithmetic with Abstraction
- Deciding an Interval Logic with Accumulated Durations
- Detecting Races in Ensembles of Message Sequence Charts
- Distributed Analysis with mu CRL: A Compendium of Case Studies
- Faster Algorithms for Finitary Games
- Flow Faster: Efficient Decision Algorithms for Probabilistic Simulations
- From Time Petri Nets to Timed Automata: An Untimed Approach
- GOAL: A Graphical Tool for Manipulating Büchi Automata and Temporal Formulae
- Generating Representation Invariants of Structurally Complex Data
- Hoare Logic for Realistically Modelled Machine Code
- Improved Algorithms for the Automata-Based Approach to Model-Checking
- JPF-SE: A Symbolic Execution Extension to Java PathFinder
- Kodkod: A Relational Model Finder
- MAVEN: Modular Aspect Verification
- Model Checking Liveness Properties of Genetic Regulatory Networks
- Model Checking Probabilistic Timed Automata with One or Two Clocks
- Model Checking on Trees with Path Equivalences
- Multi-objective Model Checking of Markov Decision Processes
- On Sampling Abstraction of Continuous Time Logic with Durations
- Optimized L*-Based Assume-Guarantee Reasoning
- PReMo : An Analyzer for P robabilistic Re cursive Mo dels
- Planned and Traversable Play-Out: A Flexible Method for Executing Scenario-Based Programs,
- Property-Driven Partitioning for Abstraction Refinement
- Refining Interface Alphabets for Compositional Verification
- Regular Model Checking Without Transducers (On Efficient Verification of Parameterized Systems)
- Replaying Play In and Play Out: Synthesis of Design Models from Scenarios by Learning
- Searching for Shapes in Cryptographic Protocols
- Shape Analysis by Graph Decomposition
- State of the Union: Type Inference Via Craig Interpolation
- Syntactic Optimizations for PSL Verification
- THERE AND BACK AGAIN: Lessons Learned on the Way to the Market
- The Heterogeneous Tool Set, Hets
- Type-Dependence Analysis and Program Transformation for Symbolic Execution
- Unfolding Concurrent Well-Structured Transition Systems
- Uppaal/DMC- Abstraction-Based Heuristics for Directed Model Checking
- VCEGAR: Verilog CounterExample Guided Abstraction Refinement
- Verifying Object-Oriented Software: Lessons and Challenges
- motor: The modestTool Environment