the proceedings contain 30 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: Interpolation and Quantifiers in Ortholattices;fun...
ISBN:
(纸本)9783031505201
the proceedings contain 30 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: Interpolation and Quantifiers in Ortholattices;function Synthesis for Maximizing model Counting;boosting Constrained Horn Solving by Unsat Core Learning;on the verification of the Correctness of a Subgraph Construction Algorithm;efficient Local Search for Nonlinear Real Arithmetic;abstractinterpretation-Based Feature Importance for Support Vector Machines;generation of Violation Witnesses by Under-Approximating abstractinterpretation;correctness Witness Validation by abstractinterpretation;project and Conquer: Fast Quantifier Elimination for checking Petri Net Reachability;parameterized verification of Disjunctive Timed Networks;Resilience and Home-Space for WSTS;Generic model checking for Modal Fixpoint Logics in COOL-MC;model-Guided Synthesis for LTL over Finite Traces.
the proceedings contain 30 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: Interpolation and Quantifiers in Ortholattices;fun...
ISBN:
(纸本)9783031505232
the proceedings contain 30 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: Interpolation and Quantifiers in Ortholattices;function Synthesis for Maximizing model Counting;boosting Constrained Horn Solving by Unsat Core Learning;on the verification of the Correctness of a Subgraph Construction Algorithm;efficient Local Search for Nonlinear Real Arithmetic;abstractinterpretation-Based Feature Importance for Support Vector Machines;generation of Violation Witnesses by Under-Approximating abstractinterpretation;correctness Witness Validation by abstractinterpretation;project and Conquer: Fast Quantifier Elimination for checking Petri Net Reachability;parameterized verification of Disjunctive Timed Networks;Resilience and Home-Space for WSTS;Generic model checking for Modal Fixpoint Logics in COOL-MC;model-Guided Synthesis for LTL over Finite Traces.
the proceedings contain 21 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: A Static Analysis of Entanglement;synthesis of Par...
ISBN:
(纸本)9783031826993
the proceedings contain 21 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: A Static Analysis of Entanglement;synthesis of Parametric Locally Symmetric Protocols from abstract Temporal Specifications;1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization;LLOR: Automated Repair of OpenMP Programs;synthesis of Controllers for Continuous Blackbox Systems;Automated Flaw Detection for Industrial Robot RESTful Service;Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study;ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks;constructing Trustworthy Smart Contracts.
the proceedings contain 21 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: A Static Analysis of Entanglement;synthesis of Par...
ISBN:
(纸本)9783031827020
the proceedings contain 21 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: A Static Analysis of Entanglement;synthesis of Parametric Locally Symmetric Protocols from abstract Temporal Specifications;1–2–3–Go! Policy Synthesis for Parameterized Markov Decision Processes via Decision-Tree Learning and Generalization;LLOR: Automated Repair of OpenMP Programs;synthesis of Controllers for Continuous Blackbox Systems;Automated Flaw Detection for Industrial Robot RESTful Service;Formally Verifiable Generated ASN.1/ACN Encoders and Decoders: A Case Study;ExpectAll: A BDD Based Approach for Link Failure Resilience in Elastic Optical Networks;constructing Trustworthy Smart Contracts.
the proceedings contain 17 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: A Generic Framework to Coarse-Grain Stochastic Reaction Netw...
ISBN:
(纸本)9783031249495
the proceedings contain 17 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: A Generic Framework to Coarse-Grain Stochastic Reaction Networks by abstractinterpretation;CosySEL: Improving SAT Solving Using Local Symmetries;sound Symbolic Execution via abstractinterpretation and Its Application to Security;result Invalidation for Incremental Modular Analyses;synthesizing History and Prophecy Variables for Symbolic model checking;solving Constrained Horn Clauses over Algebraic Data Types;ARENA: Enhancing abstract Refinement for Neural Network verification;SMT-Based modeling and verification of Spiking Neural Networks: A Case Study;StaticPersist: Compiler Support for PMEM Programming;symbolic abstract Heaps for Polymorphic Information-Flow Guard Inference;satisfiability Modulo Custom theories in Z3;bayesian Parameter Estimation with Guarantees via Interval Analysis and Simulation;a Pragmatic Approach to Stateful Partial Order Reduction;compositional verification of Stigmergic Collective Systems;efficient Interprocedural Data-Flow Analysis Using Treedepth and Treewidth.
the proceedings contain 27 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: Demand control-flow analysis;effect-driven flow analysis;typ...
ISBN:
(纸本)9783030112448
the proceedings contain 27 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: Demand control-flow analysis;effect-driven flow analysis;type-directed bounding of collections in reactive programs;solving and interpolating constant arrays based on weak equivalences;a decidable logic for tree data-structures with measurements;a practical algorithm for structure embedding;EUFORIA: Complete software model checking with uninterpreted functions;Fast BGP simulation of large datacenters;verification of an industrial asynchronous leader election algorithm using abstractions and parametric model checking;program synthesis with equivalence reduction;application of abstractinterpretation to the automotive electronic control system;syntactic partial order compression for probabilistic reachability;termination of nondeterministic probabilistic programs;parametric timed broadcast protocols;Flat model checking for counting LTL using quantifier-free presburger arithmetic;a parallel relation-based algorithm for symbolic bisimulation minimization;combining refinement of parametric models with goal-oriented reduction of dynamics;mechanically proving determinacy of hierarchical block diagram translations;minimal synthesis of string to string functions from examples;automatic program repair using formal verification and expression templates;lazy but effective functional synthesis;static analysis of binary code with memory indirections using polyhedra;disjunctive relational abstractinterpretation for interprocedural program analysis;exploiting pointer analysis in memory models for deductive verification;small faults grow up - verification of error masking robustness in arithmetically encoded programs.
the proceedings contain 24 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: Invariant generation for multi-path loops with polynomial as...
ISBN:
(纸本)9783319737201
the proceedings contain 24 papers. the special focus in this conference is on verification, model checking, and abstract interpretation. the topics include: Invariant generation for multi-path loops with polynomial assignments;analyzing guarded protocols: Better cutoffs, more systems, more expressivity;refinement types for ruby;modular analysis of executables using on-demand heyting completion;Learning to complement büchi automata;p5: Planner-less proofs of probabilistic parameterized protocols;co-design and verification of an available file system;abstraction-based interaction model for synthesis;generating tests by example;gradual program verification;a logical system for modular information flow verification;on constructivity of galois connections;Revisiting MITL to fix decision procedures;selfless interpolation for infinite-state model checking;an abstractinterpretation framework for the round-off error analysis of floating-point programs;Automatic verification of RMA programs via abstraction extrapolation;scalable approximation of quantitative information flow in programs;code obfuscation against abstract model checking attacks;abstract code injection: A semantic approach based on abstract non-interference;a framework for computer-aided design of educational domain models;automatic verification of intermittent systems;on abstraction and compositionality for weak-memory linearisability.
modelchecking trees generated by Higher-Order Recursion Schemes (HORS) of order k against Alternating Parity Tree-Automata (APT) is known to be a k-EXPTIME-complete problem (Ong'06). We exhibit a natural fragment...
详细信息
ISBN:
(纸本)9783031826993;9783031827006
modelchecking trees generated by Higher-Order Recursion Schemes (HORS) of order k against Alternating Parity Tree-Automata (APT) is known to be a k-EXPTIME-complete problem (Ong'06). We exhibit a natural fragment of HORS, called tail-recursive HORS, and a restricted APT model, called bounded-alternation APT, such that the problem of model checking trees generated by order-k tail-recursive HORS against bounded-alternation APT is k-1-EXPSPACE-complete. the upper bound is achieved by converting the problem into an alternating reachability game, the lower one via reduction from a tiling problem.
Many distributed systems require temporal properties to hold for correctness. model checking can verify these properties on a small system but it doesn't scale for arbitrarily large systems. this work presents a n...
详细信息
ISBN:
(纸本)9783031826993;9783031827006
Many distributed systems require temporal properties to hold for correctness. model checking can verify these properties on a small system but it doesn't scale for arbitrarily large systems. this work presents a new method for proving that temporal properties verified on a small system extend to an arbitrarily large system when that system has a ring topology. It uses a model checker to prove temporal properties and properties of a partial order of events in the system. It then admits the partial order properties as axioms in a theorem prover and proves a conformance relation between an arbitrary-sized ring of nodes and the model-checked base case. the conformance relation is used to prove that adding a new node to the ring does not affect the possible states of the existing nodes in the system and therefore any properties proven in the small system continue to hold in an arbitrarily large system. We demonstrate the approach in a case study of a nontrivial distributed protocol that is used by the MyCHIP's digital currency to clear credit.
We address the verification problem for concurrent program that dynamically create (fork) new threads or destroy (join) existing threads. We present a reduction to the verification problem for concurrent programs with...
详细信息
ISBN:
(纸本)9783031505201;9783031505218
We address the verification problem for concurrent program that dynamically create (fork) new threads or destroy (join) existing threads. We present a reduction to the verification problem for concurrent programs with a fixed number of threads. More precisely, we present petrification, a transformation from programs with dynamic thread management to an existing, Petri net-based formalism for programs with a fixed number of threads. Our approach is implemented in a software model checking tool for C programs that use the pthreads API.
暂无评论