Verifying Multithreaded Recursive Programs with Integer Variables

DOI10.1016/j.entcs.2009.05.036zbMath1347.68069OpenAlexW2043599013MaRDI QIDQ5179057

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

verificationrewriting systemsprogram analysistree automatasynchronisationinteger variablesmultithreaded programs with procedure calls

Mathematics Subject Classification ID

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

Uses Software

• Maude
• MAGIC

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Summarizing procedures in concurrent programs
• Abstract Regular Tree Model Checking of Complex Dynamic Data Structures
• The integration of functions into logic programming: From theory to practice
• Efficient algorithms for pre* and post* on interprocedural parallel flow graphs
• Lazy abstraction
• FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science
• Term Rewriting and Applications
• Tools and Algorithms for the Construction and Analysis of Systems

This page was built for publication: Verifying Multithreaded Recursive Programs with Integer Variables