A fixpoint calculus for local and global program flows

DOI10.1145/1111037.1111051zbMath1370.68051OpenAlexW2155627592MaRDI QIDQ5348921

P. Madhusudan, Swarat Chaudhuri, Rajeev Alur

Publication date: 21 August 2017

Published in: Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages (Search for Journal in Brave)

Full work available at URL: https://repository.upenn.edu/cgi/viewcontent.cgi?article=1533&context=cis_papers

zbMATH Keywords

verification\(\mu\)-calculusmodel checkingspecificationgamesprogram logicpushdown systemsinfinite-state

Mathematics Subject Classification ID

Formal languages and automata (68Q45) Modal logic (including the logic of norms) (03B45) Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (12)

A Branching Time Variant of CaRet ⋮ Model Checking Procedural Programs ⋮ Summarization for termination: No return! ⋮ Colored nested words ⋮ Propositional dynamic logic with recursive programs ⋮ Reducing behavioural to structural properties of programs with procedures ⋮ Interval Temporal Logic for Visibly Pushdown Systems ⋮ A structural/temporal query language for business processes ⋮ Regular languages of nested words: fixed points, automata, and synchronization ⋮ A saturation method for the modal \(\mu \)-calculus over pushdown systems ⋮ Temporal logics with language parameters ⋮ Nested Sibling Tree Automata

This page was built for publication: A fixpoint calculus for local and global program flows