Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings

摘要: Invited Talks.- Policy Monitoring in First-Order Temporal Logic.- Retrofitting Legacy Code for Security.- Quantitative Information Flow: From Theory to Practice?.- Memory Management Concurrent Algorithms.- Tutorials.- ABC: An Academic Industrial-Strength Verification Tool.- There's Plenty of Room at the Bottom: Analyzing and Verifying Machine Code.- Constraint Solving Program Verification: Practice by Example.- Session 1. Software Model Checking.- Invariant Synthesis Programs Manipulating Lists with Unbounded Data.- Termination Analysis Compositional Transition Invariants.- Lazy Annotation Testing Verification.- The Static Driver Verifier Research Platform.- Dsolve: Safety via Liquid Types.- Contessa: Concurrency Augmented Symbolic Analysis.- 2. Checking Automata.- Simulation Subsumption Ramsey-Based Buchi Automata Universality Inclusion Testing.- Efficient Emptiness Check Timed 3. Tools.- Merit: Interpolating Model-Checker.- Breach, A Toolbox Parameter Hybrid Systems.- Jtlv: Framework Developing Petruchio: Dynamic Networks Nets.- 4. Counter Systems Quantized Feedback Control Discrete Time Linear Probabilistic Logical Product Approach Zonotope Intersection.- Fast Acceleration Ultimately Periodic Relations.- Abstraction-Refinement Artificial Neural Networks.- 5. Consistency.- Fences Weak Models.- Generating Litmus Tests Contrasting Consistency 6. Hardware Low Level Directed Proof Generation Low-Level Implementations High-Level Datatypes.- Automatic Inductive Invariants from Microarchitectural Models Communication Fabrics.- Reachability Pushdown Hardware/Software Co-verification.- 7. LTSmin: Distributed Reachability.- libalf: Learning Framework.- 8. Synthesis.- Bounded Measuring Synthesizing Environments.- Achieving through Robustness Presence Liveness.- RATSY - New Requirements Tool Comfusy: Complete Functional 9. I.- Universal Causality Graphs: Precise Happens-Before Detecting Bugs Programs.- Automatically Proving Linearizability.- Linearizability List Implementations.- Local Global Abstract Executions.- 10. Reasoning.- Automated Assume-Guarantee Reasoning Implicit Learning.- Component Interfaces May Must Abstractions.- Dash Fairness SPLIT: LTL Verifier.- 11. Checker AADL.- PESSOA: Embedded Controller 12. Decision Procedures.- On Array Elements.- Quantifier Elimination Enumeration.- 13. II.- Underapproximations.- Phase Multi-stack Model-Checking Parameterized Using Interfaces.- Cutoff Detection 14. PARAM: Parametric Markov Gist: Solver Games.- NuSMV Extension Graded-CTL Checking.