Verification, Model Checking, and Abstract Interpretation 22nd International Conference, VMCAI 2021, Copenhagen, Denmark, January 17–19, 2021, Proceedings
This book constitutes the proceedings of the 22nd International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2021, which was held virtually during January 17-19, 2021. The conference was planned to take place in Copenhagen, Denmark, but changed to an online event du...
| Other Authors: | , , |
|---|---|
| Format: | eBook |
| Language: | English |
| Published: |
Cham
Springer International Publishing
2021, 2021
|
| Edition: | 1st ed. 2021 |
| Series: | Theoretical Computer Science and General Issues
|
| Subjects: | |
| Online Access: | |
| Collection: | Springer eBooks 2005- - Collection details see MPG.ReNa |
Table of Contents:
- Invited Papers
- Model Checking Algorithms for Hyperproperties
- Algebra-based Synthesis of Loops and their Invariants
- Generative Program Analysis and Beyond: The Power of Domain-Specific Languages
- Hyperproperties and Infinite-state Systems
- Compositional Model Checking for Multi-Properties
- Decomposing Data Structure Commutativity Proofs with mn-Differencing
- Proving the existence of fair paths in infinite-state systems
- A Self-Certifying Compilation Framework for WebAssembly
- Concurrent and Distributed Systems
- Concurrent Correctness in Vector Space
- Verification of Concurrent Programs Using Petri Net Unfoldings
- Eliminating Message Counters in Synchronous Threshold Automata
- A Reduction Theorem for Randomized Distributed Algorithms under Weak Adversaries
- Checking
- Runtime Abstract Interpretation for Numerical Accuracy and Robustness
- Twinning automata and regular expressions for string static analysis
- Unbounded Procedure Summaries from Bounded Environments
- Syntax-Guided Synthesis for Lemma Generation in Hardware Model Checking
- Synthesis and Repair
- Approximate Bit Dependency Analysis to Identify Program Synthesis Problems as Infeasible
- Automated Repair of Heap-Manipulating Programs using Deductive Synthesis
- GPURepair: Automated Repair of GPU Kernels
- Applications
- A Synchronous Effects Logic for Temporal Verification of Pure Esterel
- A Design of GPU-Based Quantitative Model Checking
- Formal Semantics and Verification of Network Based Biocomputation Circuits
- Netter: Probabilistic, Stateful Network Models,. Decision Procedures
- Deciding the Bernays-Schoenfinkel Fragment over Bounded Difference Constraints by Simple Clause Learning over Theories
- Incremental Search for Conflict and Unit Instances of Quantified Formulas with E-Matching
- On Preprocessing for Weighted MaxSAT
- Compositional Satisfiability Solving in Separation Logic