Runtime complexity analysis of logically constrained rewriting

DOI10.1007/978-3-030-68446-4_2OpenAlexW3133800324MaRDI QIDQ2119101

Georg Moser, Sarah Winkler

Publication date: 23 March 2022

Full work available at URL: https://arxiv.org/abs/2012.06370

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

ATLAS: automated amortised complexity analysis of self-adjusting data structures ⋮ Analysing parallel complexity of term rewriting ⋮ Type-based analysis of logarithmic amortised complexity ⋮ Runtime complexity analysis of logically constrained rewriting

Uses Software

• Yices
• z3
• Maude
• Ctrl
• KITTeL
• TiML
• TcT

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• A combination framework for complexity
• All about Maude -- a high-performance logical framework. How to specify, program and verify systems in rewriting logic. With CD-ROM.
• Loop detection by logically constrained term rewriting
• From Jinja bytecode to term rewriting: a complexity reflecting transformation
• A coinductive approach to proving reachability properties in logically constrained term rewriting systems
• Runtime complexity analysis of logically constrained rewriting
• Non-polynomial worst-case analysis of recursive programs
• Analyzing innermost runtime complexity of term rewriting by dependency pairs
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Term Rewriting with Logical Constraints
• Resource Usage Analysis of Logic Programs via Abstract Interpretation Using Sized Types
• On the Inference of Resource Usage Upper and Lower Bounds
• Analysing the complexity of functional programs: higher-order meets first-order
• Constrained Term Rewriting tooL
• Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis
• Automated Complexity Analysis Based on the Dependency Pair Method
• Proving Termination of Integer Term Rewriting
• SPEED: Symbolic Complexity Bound Analysis
• Term Rewriting and All That
• Complexity Analysis for Java with AProVE
• Verifying Procedural Programs via Constrained Rewriting Induction
• Towards automatic resource bound analysis for OCaml
• Termination Analysis of C Programs Using Compiler Intermediate Languages
• Verification, Model Checking, and Abstract Interpretation

This page was built for publication: Runtime complexity analysis of logically constrained rewriting