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

integer variablesmultithreaded programs with procedure callsprogram analysisrewriting systemssynchronisationtree automataverification

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) 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

• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• 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
• 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?)
• 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

Cited in

(5)

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

Describes a project that uses

Uses Software

• Maude
• MAGIC

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)