Rewriting modulo SMT and open system analysis
From MaRDI portal
Publication:347384
DOI10.1016/j.jlamp.2016.10.001zbMath1353.68156OpenAlexW2531460317MaRDI QIDQ347384
José Meseguer, Camilo Rocha, César A. Muñoz
Publication date: 30 November 2016
Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.jlamp.2016.10.001
Specification and verification (program logics, model checking, etc.) (68Q60) Grammars and rewriting systems (68Q42)
Related Items (6)
Executing and verifying higher-order functional-imperative programs in Maude ⋮ Operationally-based program equivalence proofs using LCTRSs ⋮ Business processes resource management using rewriting logic and deep-learning-based predictive monitoring ⋮ Strategies in conditional narrowing modulo SMT plus axioms ⋮ Generalized rewrite theories, coherence completion, and symbolic methods ⋮ Programming and symbolic computation in Maude
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Sufficient completeness verification for conditional and constrained TRS
- On deciding satisfiability by theorem proving with speculative inferences
- Complete symbolic reachability analysis using back-and-forth narrowing
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Conditional rewriting logic as a unified model of concurrency
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- A theory of timed automata
- Combining unification algorithms
- Combining symbolic constraint solvers on algebraic domains
- Equational rules for rewriting logic
- Kronos: A verification tool for real-time systems
- Uppaal in a nutshell
- Unification in the union of disjoint equational theories: Combining decision procedures
- Proving operational termination of membership equational programs
- Semantic foundations for generalized rewrite theories
- Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
- Term Rewriting with Logical Constraints
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Rewriting Modulo SMT and Open System Analysis
- Abstract Logical Model Checking of Infinite-State Systems Using Narrowing
- Solving SAT and SAT Modulo Theories
- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Towards SMT Model Checking of Array-Based Systems
- Automated Induction with Constrained Tree Automata
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Superposition Modulo Linear Arithmetic SUP(LA)
- Simplification by Cooperating Decision Procedures
- Operational Termination of Conditional Rewriting with Built-in Numbers and Semantic Data Structures
- Operational Termination of Membership Equational Programs: the Order-Sorted Way
- On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs
- A Completion Algorithm for Lattice Tree Automata
- MCMT: A Model Checker Modulo Theories
- Perspectives of System Informatics
- Constraint-based deductive model checking
This page was built for publication: Rewriting modulo SMT and open system analysis
