NDLI: A fixpoint calculus for local and global program flows

Please wait, while we are loading the content...

Why dependent types matter

The next 700 data description languages

A hierarchical model of data locality

Simplifying reductions

Formal certification of a compiler back-end or: programming a compiler with a proof assistant

Engineering with logic: HOL specification and symbolic-evaluation testing for TCP implementations

Decidability and proof systems for language-based noninterference relations

On flow-sensitive security types

A logic for information flow in object-oriented programs

Polymorphic regular tree types and patterns

Verifying properties of well-founded linked lists

Environment analysis via ΔCFA

Small bisimulations for reasoning about higher-order imperative programs

A fixpoint calculus for local and global program flows

The Scala experiment: can we provide better language support for component systems?

Adventures in time and space

N-synchronous Kahn networks: a relaxed model of synchrony for real-time systems

Compiler-directed channel allocation for saving power in on-chip networks

Fast and loose reasoning is morally correct

Modular set-based analysis from contracts

Stratified type inference for generalized algebraic data types

Hybrid type checking

A polymorphic modal type system for lisp-like multi-staged languages

The next mainstream programming language: a game developer's perspective

A virtual class calculus

Interruptible iterators

Specifying C++ concepts

Frame rules from answer types for code pointers

Certified assembly programming with embedded code pointers

Associating synchronization constraints with data in an object-oriented language

Autolocker: synchronization inference for atomic sections

Protecting representation with effect encapsulation

The essence of command injection attacks in web applications

Harmless advice

A verifiable SSA program representation for aggressive compiler optimization

Staged allocation: a compositional technique for specifying and implementing procedure calling conventions

A fixpoint calculus for local and global program flows

Content Provider	ACM Digital Library
Author	Chaudhuri, Swarat Madhusudan, P. Alur, Rajeev
Abstract	We define a new fixpoint modal logic, the visibly pushdown μ-calculus (VP-μ), as an extension of the modal μ-calculus. The models of this logic are execution trees of structured programs where the procedure calls and returns are made visible. This new logic can express pushdown specifications on the model that its classical counterpart cannot, and is motivated by recent work on visibly pushdown languages [4]. We show that our logic naturally captures several interesting program specifications in program verification and dataflow analysis. This includes a variety of program specifications such as computing combinations of local and global program flows, pre/post conditions of procedures, security properties involving the context stack, and interprocedural dataflow analysis properties. The logic can capture flow-sensitive and inter-procedural analysis, and it has constructs that allow skipping procedure calls so that local flows in a procedure can also be tracked. The logic generalizes the semantics of the modal μ-calculus by considering summaries instead of nodes as first-class objects, with appropriate constructs for concatenating summaries, and naturally captures the way in which pushdown models are model-checked. The main result of the paper is that the model-checking problem for VP-μ is effectively solvable against pushdown models with no more effort than that required for weaker logics such as CTL. We also investigate the expressive power of the logic VP-μ: we show that it encompasses all properties expressed by a corresponding pushdown temporal logic on linear structures (caret [2]) as well as by the classical μ-calculus. This makes VP-μ the most expressive known program logic for which algorithmic software model checking is feasible. In fact, the decidability of most known program logics (μ-calculus, temporal logics LTL and CTL, caret, etc.) can be understood by their interpretation in the monadic second-order logic over trees. This is not true for the logic VP-μ, making it a new powerful tractable program logic.
Starting Page	153
Ending Page	165
Page Count	13
File Format	PDF
ISBN	1595930272
DOI	10.1145/1111037.1111051
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2006-01-11
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Games Pushdown systems Μ-calculus Specification Verification Infinite-state Logic Model-checking
Content Type	Text
Resource Type	Article

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

A fixpoint calculus for local and global program flows

A fixpoint calculus for local and global program flows (2006).

Software model checking using languages of nested trees

A Fixpoint Calculus for Local and Global Program Flows (2006)

Global vs. local model checking: A comparison of verification techniques for infinite state systems (2004)

Local model checking in park's µ-calculus (1996).

About the decision of reachability for register machines

Pushdown Processes: Games and Model Checking (1996)

Three notes on the complexity of model checking fixpoint logic with chop

A fixpoint calculus for local and global program flows

Similar Documents

A fixpoint calculus for local and global program flows

A fixpoint calculus for local and global program flows (2006).

Software model checking using languages of nested trees

A Fixpoint Calculus for Local and Global Program Flows (2006)

Global vs. local model checking: A comparison of verification techniques for infinite state systems (2004)

Local model checking in park's µ-calculus (1996).

About the decision of reachability for register machines

Pushdown Processes: Games and Model Checking (1996)

Three notes on the complexity of model checking fixpoint logic with chop

A fixpoint calculus for local and global program flows