Verification, Model Checking, and Abstract Interpretation : 18th International Conference, VMCAI 2017, Paris, France, January 15–17, 2017, Proceedings /
| Autor Corporativo: | |
|---|---|
| Otros Autores: | , |
| Formato: | eBook |
| Lenguaje: | English |
| Publicado: |
Cham :
Springer International Publishing : Imprint: Springer,
2017.
|
| Edición: | 1st ed. 2017. |
| Colección: | Theoretical Computer Science and General Issues ;
10145 |
| Materias: |
Tabla de Contenidos:
- Bringing LTL Model Checking to Biologists
- Verified Concurrent Code: Tricks of the Trade
- Detecting Strict Aliasing Violations in the Wild
- Effective Bug Finding in C Programs with Shape and Effect Abstractions
- Synthesizing Non-Vacuous Systems
- Static Analysis of Communicating Process Using Symbolic Transducers
- Reduction of Workflow Nets for Generalized Soundness Verification
- Structuring Abstract Interpreters through State and Value Abstractions
- Matching Multiplications in Bit-Vector Formulas
- Independence Abstractions and Models of Concurrency
- Complete Abstractions and Subclassical Modal Logics
- Using Abstract Interpretation to Correct Synchronization Faults
- Property Directed Reachability for Proving Absence of Concurrent Modification Errors
- Stabilizing Floating-Point Programs Using Provenance Analysis
- Dynamic Reductions for Model Checking Concurrent Software
- Synthesising Strategy Improvement and Recursive Algorithms for Solving 2.5 Player Parity Games
- Counterexample Validation and Interpolation-Based Refinement for Forest Automata
- Block-wise Abstract Interpretation by Combining Abstract Domains with SMT
- Solving Nonlinear Integer Arithmetic with MCSat
- Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
- Efficient Elimination of Redundancies in Polyhedra Using Raytracing
- Precise Thread-Modular Abstract Interpretation of Concurrent Programs Using Relational Interference Abstractions
- Detecting All High-Level Dataraces in an RTOS Kernel
- Reachability for Dynamic Parametric Processes
- Conjunctive Abstract Interpretation Using Paramodulation
- Reasoning in the Bernays-Schonfinkel-Ramsey Fragment of Separation Logic
- Finding Relevant Templates via the Principal Component Analysis
- Sound Bit-Precise Numerical Domains
- IC3 - Flipping the E in ICE
- Partitioned Memory Models for Program Analysis.