scientific article
From MaRDI portal
Publication:2754081
zbMath0974.68517MaRDI QIDQ2754081
Yuan Lu, Helmut Veith, Orna Grumberg, Somesh Jha, Edmund M. Clarke
Publication date: 11 November 2001
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
Related Items
Tuning as convex optimisation: a polynomial tuner for multi-parametric combinatorial samplers, Whale: An Interpolation-Based Algorithm for Inter-procedural Verification, Lazy Synthesis, Predicate Abstraction for Program Verification, Verification of Hybrid Systems, The Complexity of Linear-Time Temporal Logic Model Repair, Bonsai: Cutting Models Down to Size, Temporal Logic Verification for Delay Differential Equations, Model Checking MSVL Programs Based on Dynamic Symbolic Execution, On Abstraction of Probabilistic Systems, Incremental SAT-Based Method with Native Boolean Cardinality Handling for the Hamiltonian Cycle Problem, Structural Reductions Revisited, Machine learning and logic: a new frontier in artificial intelligence, Verification Modulo theories, Interpolation with guided refinement: revisiting incrementality in SAT-based unbounded model checking, Neural Network Verification Using Residual Reasoning, Symbolic analysis of linear hybrid automata -- 25 years later, Parameter synthesis in Markov models: a gentle survey, The Right Kind of Non-Determinism: Using Concurrency to Verify C Programs with Underspecified Semantics, Enhancing active model learning with equivalence checking using simulation relations, Symbolic encoding of LL(1) parsing and its applications, Using Counterexample Analysis to Minimize the Number of Predicates for Predicate Abstraction, Boosting robustness verification of semantic feature neighborhoods, The Birth of Model Checking, Solving constrained Horn clauses over algebraic data types, Automated Assume-Guarantee Reasoning by Abstraction Refinement, Probabilistic CEGAR, Automatic Abstraction Refinement in Neural Network Verification using Sensitivity Analysis, Unnamed Item, Predicate Abstraction in Program Verification: Survey and Current Trends, Parametric Verification of Weighted Systems, Automatic Data-Abstraction in Model Checking Multi-Agent Systems, Counterexample-Guided Refinement of Template Polyhedra, Abstraction-Based Algorithm for 2QBF, Smaller Abstractions for ∀CTL* without Next, Complexity and Algorithms for Monomial and Clausal Predicate Abstraction, Predicate Abstraction in a Program Logic Calculus, Dynamic Path Reduction for Software Model Checking, An Assume Guarantee Approach for Checking Quantified Array Assertions, Satisfiability Solving and Model Generation for Quantified First-Order Logic Formulas, Deriving Bisimulations by Simplifying Partitions, Internal and External Logics of Abstract Interpretations, Verifying Reference Counting Implementations, On-the-Fly Techniques for Game-Based Software Model Checking, Conditional Probabilities over Probabilistic and Nondeterministic Systems, Efficient Automatic STE Refinement Using Responsibility, Distributed and Predictable Software Model Checking, Applying CEGAR to the Petri Net State Equation, Abstraction Refinement for Quantified Array Assertions, Refinement of Trace Abstraction, Abstract Interpretation from a Topological Perspective, An Inverse Method for Parametric Timed Automata, Sound and Complete Abstract Graph Transformation, Abstract Counterexamples for Non-disjunctive Abstractions, Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*, CAQE and QuAbS: Abstraction Based QBF Solvers, Verification of Random Graph Transformation Systems, Automated formal analysis and verification: an overview, Symbolic and Structural Model-Checking, A complete refinement procedure for regular separability of context-free languages, Advanced algorithms for abstract dialectical frameworks based on complexity analysis of subclasses and SAT solving, An approximation framework for solvers and decision procedures, A layered algorithm for quantifier elimination from linear modular constraints, Counterexample-guided predicate abstraction of hybrid systems, Verification of SpecC using predicate abstraction, Lattice-based refinement in bounded model checking, A program analysis framework for \textit{tccp} based on abstract interpretation, Projecting transition systems: overcoming state explosion in concurrent system verification, Why does Astrée scale up?, Faster pushdown reachability analysis with applications in network verification, Property-directed verification and robustness certification of recurrent neural networks, Lazy slicing for state-space exploration, Verifying data refinements using a model checker, GSTE is partitioned model checking, Satisfiability and synthesis modulo oracles, Predicate diagrams for the verification of real-time systems, When not losing is better than winning: abstraction and refinement for the full \(\mu\)-calculus, Effect-polymorphic behaviour inference for deadlock checking, LCTD: test-guided proofs for C programs on LLVM, Abstraction for model checking multi-agent systems, Offline and online monitoring of scattered uncertain logs using uncertain linear dynamical systems, A game-based abstraction-refinement framework for Markov decision processes, An invariant-based approach to the verification of asynchronous parameterized networks, Abstraction based verification of stability of polyhedral switched systems, Robust synthesis for real-time systems, System-level state equality detection for the formal dynamic verification of legacy distributed applications, Extracting counterexamples induced by safety violation in linear hybrid systems, Hybrid automata-based CEGAR for rectangular hybrid systems, Consistency-preserving refactoring of refinement structures in Event-B models, Efficient verification of concurrent systems using local-analysis-based approximations and SAT solving, Minimal counterexamples for linear-time probabilistic verification, Combinatorial abstraction refinement for feasibility analysis of static priorities, Verifying a scheduling protocol of safety-critical systems, Preface of the special issue in memoriam Helmut Veith, \textsc{NeVer}: a tool for artificial neural networks verification, SAT-based verification for timed component connectors, SAT-solving in CSP trace refinement, Verification of multi-linked heaps, Consistency and refinement for interval Markov chains, Deadlock checking by a behavioral effect system for lock handling, Counterexample-guided abstraction refinement for symmetric concurrent programs, An automatic method for the dynamic construction of abstractions of states of a formal model, Learning inductive invariants by sampling from frequency distributions, Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol, SAT-LP-IIS joint-directed path-oriented bounded reachability analysis of linear hybrid automata, An extension of lazy abstraction with interpolation for programs with arrays, Analysis of correct synchronization of operating system components, Predicate extension of symbolic memory graphs for the analysis of memory safety correctness, Learning to divide and conquer: applying the \(L^*\) algorithm to automate assume-guarantee reasoning, Verification of evolving software via component substitutability analysis, Automatic symbolic compositional verification by learning assumptions, A framework for the verification of infinite-state graph transformation systems, Parameter synthesis for hierarchical concurrent real-time systems, Property-directed incremental invariant generation, Model checking duration calculus: a practical approach, Unbounded procedure summaries from bounded environments, Equational abstractions, Verification of Boolean programs with unbounded thread creation, Combining search space partition and abstraction for LTL model checking, On relative and probabilistic finite counterability, Efficient SAT-based bounded model checking for software verification, Replacing conjectures by positive knowledge: inferring proven precise worst-case execution time bounds using symbolic execution, Component-wise incremental LTL model checking, Abstraction and mining of traces to explain concurrency bugs, SMT-based model checking for recursive programs, Loop summarization using state and transition invariants, An efficient approach for abstraction-refinement in model checking, Correctness kernels of abstract interpretations, Experience of improving the BLAST static verification tool, Synthesis and infeasibility analysis for stochastic models of biochemical systems using statistical model checking and abstraction refinement, Verification and falsification of programs with loops using predicate abstraction, Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols, Competent predicate abstraction in model checking, Predicate abstraction in a program logic calculus, Incompleteness of states w.r.t. traces in model checking, Solving games via three-valued abstraction refinement, Actor-based slicing techniques for efficient reduction of Rebeca models, A survey of safety and trustworthiness of deep neural networks: verification, testing, adversarial attack and defence, and interpretability, Compositional SCC analysis for language emptiness, Safe \& robust reachability analysis of hybrid systems, Unbounded-time safety verification of guarded LTI models with inputs by abstract acceleration, Solving finite-linear-path CTL-formulas using the CEGAR approach, Partial predicate abstraction and counter-example guided refinement, Improving neural network verification through spurious region guided refinement, Counter Abstraction in the CSP/FDR setting, A shape graph logic and a shape system, Predicate Abstraction for Dense Real-Time Systems1 1This research was supported by the National Science Foundation under grants CCR-00-82560 and CCR-00-86096 and by NASA Langley Research Center under contract B09060051 and Cooperative Agreement NCC-1-399 with Honeywell Minneapolis. Most of this research has been conducted while the first author was visiting SRI International, July/August 2001., View-Augmented Abstractions, A theory of structural stationarity in the \(\pi\)-calculus, CEGAR for compositional analysis of qualitative properties in Markov decision processes, NIL: learning nonlinear interpolants, Using state abstractions to compute personalized contrastive explanations for AI agent behavior, A Three-Value Abstraction Technique for the Verification of Epistemic Properties in Multi-agent Systems, Efficient Craig interpolation for linear Diophantine (dis)equations and linear modular equations, Integration of verification methods for program systems, CPCES: a planning framework to solve conformant planning problems through a counterexample guided refinement, A semantic framework for the abstract model checking of tccp programs, Automated planning as an early verification tool for distributed control, A framework for compositional verification of multi-valued systems via abstraction-refinement
Uses Software
