CONCUR 2005 – Concurrency Theory

DOI10.1007/11539452MaRDI QIDQ5897503zbMATH OpenOpenAlexFDO

Authors Aaron R. Bradley, Zohar Manna, Henny B. Sipma

Publication date 1 November 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/11539452

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• TERMINATION ANALYSIS OF LINEAR LOOPS
• On termination of integer linear loops
• Termination analysis of linear loop programs
• Termination of linear loops over the integers
• On the termination of integer loops
• scientific article; zbMATH DE number 6401180
• Automated Technology for Verification and Analysis
• Reflections on termination of linear loops
• Symbolic termination analysis of solvable loops

Cited in

(20)

• Convergence: integrating termination and abort-freedom
• Algebraic model checking for discrete linear dynamical systems
• Ranking function synthesis for bit-vector relations
• Proving total correctness and generating preconditions for loop programs via symbolic-numeric computation methods
• On the termination of integer loops
• Non-termination Sets of Simple Linear Loops
• Loop Summarization and Termination Analysis
• TERMINATION ANALYSIS OF LINEAR LOOPS
• Recent advances in program verification through computer algebra
• Taming the Wrapping of Integer Arithmetic
• Generating exact nonlinear ranking functions by symbolic-numeric hybrid method
• Proving termination of nonlinear command sequences
• Termination of linear loops over the integers
• Automatic verification of counter systems with ranking function
• Programs with lists are counter automata
• Automated Technology for Verification and Analysis
• scientific article; zbMATH DE number 6401180 (Why is no real title available?)
• Ranking functions for linear-constraint loops
• What's decidable about discrete linear dynamical systems?
• Lower-bound synthesis using loop specialization and Max-SMT

This page was built for publication: CONCUR 2005 – Concurrency Theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5897503)