Verification, Model Checking, and Abstract Interpretation
Springer International Publishing (Verlag)
978-3-030-67066-5 (ISBN)
The 23 papers presented in this volume were carefully reviewed from 48 submissions. VMCAI provides a forum for researchers working on verification, model checking, and abstract interpretation and facilitates interaction, cross-fertilization, and advancement of hybrid methods that combine these and related areas. The papers presented in this volume were organized in the following topical sections: hyperproperties and infinite-state systems; concurrent and distributed systems; checking; synthesis and repair; applications; and decision procedures.
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.
| Erscheinungsdatum | 13.01.2021 |
|---|---|
| Reihe/Serie | Lecture Notes in Computer Science | Theoretical Computer Science and General Issues |
| Zusatzinfo | XV, 604 p. 212 illus., 108 illus. in color. |
| Verlagsort | Cham |
| Sprache | englisch |
| Maße | 155 x 235 mm |
| Gewicht | 926 g |
| Themenwelt | Mathematik / Informatik ► Informatik ► Software Entwicklung |
| Informatik ► Theorie / Studium ► Algorithmen | |
| Schlagworte | architecture verification and validation • Artificial Intelligence • Automata Theory • computer programming • Computer systems • distributed computer systems • Embedded Systems • Engineering • Formal Languages • Formal Logic • formal methods • graph theory • Mathematics • Model Checking • parallel processing systems • software architecture • Software Defect Analysis • Software Design • Software engineering • Software Quality • Software Verification • theoretical computer science • verification • Verification and Validation |
| ISBN-10 | 3-030-67066-X / 303067066X |
| ISBN-13 | 978-3-030-67066-5 / 9783030670665 |
| Zustand | Neuware |
| Haben Sie eine Frage zum Produkt? |
aus dem Bereich
