Verifying multithreaded recursive programs with integer variables

DOI10.1016/J.ENTCS.2009.05.036MaRDI QIDQ5179057zbMATH OpenOpenAlexFDO

Authors Narjes Ben Rajeb, Brahim Nasraoui, Riadh Robbana, Tayssir Touili

Publication date 19 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.05.036

zbMATH Keywords

verificationsynchronisationinteger variablestree automatarewriting systemsprogram analysismultithreaded programs with procedure calls

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Decidable models of integer-manipulating programs with recursive parallelism
• Decidable models of integer-manipulating programs with recursive parallelism
• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Weakly-synchronized ground tree rewriting (with applications to verifying multithreaded programs)
• Complexity of pattern-based verification for multithreaded programs

Cites work

• scientific article; zbMATH DE number 2043522 (Why is no real title available?)
• scientific article; zbMATH DE number 1744961 (Why is no real title available?)
• scientific article; zbMATH DE number 1903379 (Why is no real title available?)
• scientific article; zbMATH DE number 1903380 (Why is no real title available?)
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• Efficient algorithms for pre* and post* on interprocedural parallel flow graphs
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Lazy abstraction
• Summarizing procedures in concurrent programs
• Term Rewriting and Applications
• The integration of functions into logic programming: From theory to practice
• Tools and Algorithms for the Construction and Analysis of Systems
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs

Cited in

(5)

• Decidable models of integer-manipulating programs with recursive parallelism
• Decidable models of integer-manipulating programs with recursive parallelism
• Multithreaded-Cartesian abstract interpretation of multithreaded recursive programs Is polynomial
• Checking a Multithreaded Algorithm with  + CAL
• Weakly-synchronized ground tree rewriting (with applications to verifying multithreaded programs)

Describes a project that uses

Uses Software

• MAGIC
• Maude

This page was built for publication: Verifying multithreaded recursive programs with integer variables

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