Rewriting modulo SMT and open system analysis
From MaRDI portal
Publication:347384
DOI10.1016/J.JLAMP.2016.10.001zbMATH Open1353.68156OpenAlexW2531460317MaRDI QIDQ347384FDOQ347384
José Meseguer, Camilo Rocha, César 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
Recommendations
- Rewriting modulo SMT and open system analysis
- Modularity in term rewriting revisited
- Modular complexity analysis for term rewriting
- A rewriting logic semantics approach to modular program analysis
- Mapping modular SOS to rewriting logic
- Analysis of rewriting-based systems as first-order theories
- Modular properties of composable term rewriting systems
- Modular rewriting semantics in practice
- Modular term rewriting systems and the termination
Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60)
Cites Work
- Kronos: A verification tool for real-time systems
- Uppaal in a nutshell
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- A theory of timed automata
- Simplification by Cooperating Decision Procedures
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Solving SAT and SAT Modulo Theories
- On deciding satisfiability by theorem proving with speculative inferences
- MCMT: A Model Checker Modulo Theories
- Unification in the union of disjoint equational theories: Combining decision procedures
- Title not available (Why is that?)
- Conditional rewriting logic as a unified model of concurrency
- Combining unification algorithms
- Combining symbolic constraint solvers on algebraic domains
- Equational rules for rewriting logic
- Proving operational termination of membership equational programs
- Semantic foundations for generalized rewrite theories
- Title not available (Why is that?)
- Title not available (Why is that?)
- 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
- 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)
- Title not available (Why is that?)
- Sufficient completeness verification for conditional and constrained TRS
- Title not available (Why is that?)
- 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
- Perspectives of System Informatics
- Constraint-based deductive model checking
- 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
Cited In (10)
- Generalized rewrite theories, coherence completion, and symbolic methods
- Business processes resource management using rewriting logic and deep-learning-based predictive monitoring
- Operationally-based program equivalence proofs using LCTRSs
- Strategies in conditional narrowing modulo SMT plus axioms
- A rewriting-logic-with-SMT-based formal analysis and parameter synthesis framework for parametric time Petri nets
- Programming and symbolic computation in Maude
- Maude2Lean: theorem proving for Maude specifications using Lean
- Incremental Rewriting Modulo SMT
- Executing and verifying higher-order functional-imperative programs in Maude
- Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
Uses Software
This page was built for publication: Rewriting modulo SMT and open system analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q347384)
