MONA
From MaRDI portal
Software:18304
No author found.
Related Items
A symbolic decision procedure for symbolic alternating finite automata ⋮ VATA: A Library for Efficient Manipulation of Non-deterministic Tree Automata ⋮ On iterating linear transformations over recognizable sets of integers ⋮ Model checking and abstraction to the aid of parameterized systems (a survey) ⋮ Unnamed Item ⋮ Model Checking Parameterized Systems ⋮ Action language verifier: An infinite-state model checker for reactive software specifications ⋮ Unnamed Item ⋮ Linear temporal logic -- from infinite to finite horizon ⋮ Formalizing the Logic-Automaton Connection ⋮ Program verification with interacting analysis plugins ⋮ Generalised multi-pattern-based verification of programs with linear linked structures ⋮ A logic of reachable patterns in linked data-structures ⋮ Efficient Symbolic Implementation of Graph Automata with Applications to Invariant Checking ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ Logic programming approach to automata-based decision procedures ⋮ Transforming graph states using single-qubit operations ⋮ Unnamed Item ⋮ Axiomatisation and decidability of multi-dimensional Duration Calculus ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Global constraint catalogue: past, present and future ⋮ Backward type inference for XML queries ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Specification and optimal reactive synthesis of run-time enforcement shields ⋮ Unnamed Item ⋮ Courcelle's theorem -- a game-theoretic approach ⋮ Decision procedures for inductive Boolean functions based on alternating automata ⋮ Filter-embedding semiring fusion for programming with MapReduce ⋮ Mechanizing the Powerset Construction for Restricted Classes of ω-Automata ⋮ Property Directed Reachability for Proving Absence of Concurrent Modification Errors ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings ⋮ Automata for the verification of monadic second-order graph properties ⋮ Automated verification of shape, size and bag properties via user-defined predicates in separation logic ⋮ An automata-theoretic approach to the verification of distributed algorithms ⋮ Generalizing input-driven languages: theoretical and practical benefits ⋮ Verification of component-based systems with recursive architectures ⋮ Spatio-temporal Model Checking for Mobile Real-Time Systems ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Practical algorithms for MSO model-checking on tree-decomposable graphs ⋮ First-order temporal logic monitoring with BDDs ⋮ Symbolic tree automata ⋮ Nested antichains for WS1S ⋮ Bounded Quantifier Instantiation for Checking Inductive Invariants ⋮ Lazy Automata Techniques for WS1S ⋮ Minimization of Visibly Pushdown Automata Using Partial Max-SAT ⋮ Unnamed Item ⋮ Complexity of fixed-size bit-vector logics ⋮ A Framework for Decentralized Physical Access Control using Finite State Automata ⋮ Synthesis from component libraries with costs ⋮ Verification and enforcement of access control policies ⋮ Automata-based symbolic string analysis for vulnerability detection ⋮ Decomposable structures, Boolean function representations, and optimization ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Regular Model Checking using Widening Techniques ⋮ Verifying a Network Invariant for All Configurations of the Futurebus+ Cache Coherence Protocol ⋮ Unnamed Item ⋮ The Model Checking Problem for Prefix Classes of Second-Order Logic: A Survey ⋮ Unnamed Item ⋮ Querying linguistic trees ⋮ Bounded treewidth as a key to tractability of knowledge representation and reasoning ⋮ Ehrenfeucht-Fraïssé goes automatic for real addition ⋮ Monitoring Metric First-Order Temporal Properties ⋮ Abstract Regular Tree Model Checking of Complex Dynamic Data Structures ⋮ From Sequential Extended Regular Expressions to NFA with Symbolic Labels ⋮ Simulations of Weighted Tree Automata ⋮ An Evaluation of Automata Algorithms for String Analysis ⋮ Combining Logic Programs and Monadic Second Order Logics by Program Transformation ⋮ A Generic Program for Minimal Subsets with Applications ⋮ Deciding Monadic Second Order Logic over $$\omega $$ ω -Words by Specialized Finite Automata ⋮ Juggrnaut: using graph grammars for abstracting unbounded heap structures ⋮ Revisiting Satisfiability and Model-Checking for CTLK with Synchrony and Perfect Recall ⋮ PITL2MONA: Implementing a Decision Procedure for Propositional Interval Temporal Logic ⋮ Complexity Hierarchies beyond Elementary ⋮ Graph operations characterizing rank-width ⋮ Don't care words with an application to the automata-based approach for real addition ⋮ Automata on finite trees ⋮ Combining Theories with Shared Set Operations ⋮ Interval Duration Logic ⋮ Unnamed Item ⋮ Theorem proving in technology transfer: The user's point of view ⋮ Declarative Dynamic Programming as an Alternative Realization of Courcelle’s Theorem ⋮ Decidability of a Hybrid Duration Calculus ⋮ Expansions of MSO by cardinality relations ⋮ Automated formal analysis and verification: an overview ⋮ Array theory of bounded elements and its applications ⋮ A second-order formulation of non-termination ⋮ Relativizations for the logic-automata connection ⋮ Computing parameterized invariants of parameterized Petri nets ⋮ wMSO theories as grammar formalisms ⋮ Efficient Runtime Verification of First-Order Temporal Properties ⋮ Structural Invariants for the Verification of Systems with Parameterized Architectures ⋮ Computing Parameterized Invariants of Parameterized Petri Nets ⋮ Unifying models ⋮ Tools and Algorithms for the Construction and Analysis of Systems ⋮ Tools and Algorithms for the Construction and Analysis of Systems ⋮ Compiler Construction ⋮ Verification, Model Checking, and Abstract Interpretation ⋮ Verified decision procedures for MSO on words based on derivatives of regular expressions ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Implementation and Application of Automata ⋮ Efficient Symbolic Representations for Arithmetic Constraints in Verification ⋮ Formal Models of Communicating Systems ⋮ Automated Deduction – CADE-20 ⋮ Automated Deduction – CADE-20 ⋮ Unnamed Item ⋮ A Practical Approach to Courcelle's Theorem ⋮ Networks of Processes with Parameterized State Space ⋮ Automatic Verification of Bossa Scheduler Properties ⋮ Symbolic model checking with rich assertional languages ⋮ Tiburon: A Weighted Tree Automata Toolkit ⋮ Unnamed Item ⋮ An Efficient Decision Procedure for Imperative Tree Data Structures ⋮ Incremental reasoning on monadic second-order logics with logic programming ⋮ An Inference-Rule-Based Decision Procedure for Verification of Heap-Manipulating Programs with Mutable Data and Cyclic Data Structures ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ Automata terms in a lazy \(\mathrm{WS}k\mathrm{S}\) decision procedure ⋮ FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science ⋮ Verification, Model Checking, and Abstract Interpretation ⋮ Verification, Model Checking, and Abstract Interpretation ⋮ Evaluation of an MSO-Solver ⋮ Turning decision procedures into disprovers ⋮ Projection for Büchi Tree Automata with Constraints between Siblings
This page was built for software: MONA
