Rewriting modulo SMT and open system analysis
From MaRDI portal
(Redirected from Publication:347384)
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
Cites work
- scientific article; zbMATH DE number 1617315 (Why is no real title available?)
- scientific article; zbMATH DE number 1688812 (Why is no real title available?)
- scientific article; zbMATH DE number 1189278 (Why is no real title available?)
- A completion algorithm for lattice tree automata
- A logical reconstruction of reachability
- A theory of timed automata
- Abstract logical model checking of infinite-state systems using narrowing
- All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
- Automated Induction with Constrained Tree Automata
- Automatic constrained rewriting induction towards verifying procedural programs
- Bounded Model Checking of Analog and Mixed-Signal Circuits Using an SMT Solver
- Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems
- Combining symbolic constraint solvers on algebraic domains
- Combining unification algorithms
- Complete symbolic reachability analysis using back-and-forth narrowing
- Conditional rewriting logic as a unified model of concurrency
- Constraint-based deductive model checking
- Dependency Pairs for Rewriting with Built-In Numbers and Semantic Data Structures
- Equational rules for rewriting logic
- Horn clauses for communicating timed systems
- Kronos: A verification tool for real-time systems
- MCMT: a model checker modulo theories
- On deciding satisfiability by theorem proving with speculative inferences
- On proving termination of constrained term rewrite systems by eliminating edges from dependency graphs
- Operational termination of conditional rewriting with built-in numbers and semantic data structures
- Operational termination of membership equational programs: the order-sorted way
- Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
- Proving operational termination of membership equational programs
- Reflection in membership equational logic, many-sorted equational logic, Horn logic with equality, and rewriting logic
- Rewriting Induction + Linear Arithmetic = Decision Procedure
- Rewriting logic semantics of a plan execution language
- Rewriting modulo SMT and open system analysis
- Semantic foundations for generalized rewrite theories
- Simplification by Cooperating Decision Procedures
- Solving SAT and SAT modulo theories, from an abstract Davis-Putnam-Logemann-Loveland procedure to \(\operatorname{DPLL}(T)\)
- Sufficient completeness verification for conditional and constrained TRS
- Superposition modulo linear arithmetic SUP(LA)
- Symbolic reachability analysis using narrowing and its application to verification of cryptographic protocols
- Term Rewriting with Logical Constraints
- Towards SMT Model Checking of Array-Based Systems
- Unification in the union of disjoint equational theories: Combining decision procedures
- Uppaal in a nutshell
Cited in
(14)- Generalized rewrite theories, coherence completion, and symbolic methods
- Business processes resource management using rewriting logic and deep-learning-based predictive monitoring
- A rewriting logic semantics for the analysis of \textsf{P} programs
- 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
- Rewriting modulo SMT and open system analysis
- Incremental Rewriting Modulo SMT
- Maude2Lean: theorem proving for Maude specifications using Lean
- Challenges in formal analysis of resilience: capturing the tradeoff between the chance of failure and the cost of success
- Executing and verifying higher-order functional-imperative programs in Maude
- Bounded model checking of multitask PLC ST programs with preemption using rewriting modulo SMT
- Symbolic analysis and parameter synthesis for time Petri nets using Maude and SMT solving
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)
