NDLI: Higher-order multi-parameter tree transducers and recursion schemes for program verification

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

Reconfigurable asynchronous logic automata: (RALA)

On the verification problem for weak memory models

Compositional may-must program analysis: unleashing the power of alternation

A simple, verified validator for software pipelining

Dependent types from counterexamples

From Boolean to quantitative notions of correctness

Nominal system T

Decision procedures for algebraic data types with abstractions

Toward a verified relational database management system

Dependent types and program equivalence

From program verification to program synthesis

Contracts made manifest

Generating compiler optimizations from proofs

Paralocks: role-based information flow control and beyond

Nested interpolants

Coarse-grained transactions

Continuity analysis of programs

A verified compiler for an impure functional language

Low-level liquid types

A theory of indirection via approximation

Automatic numeric abstractions for heap-manipulating programs

Counterexample-guided focus

Pure subtype systems

Abstraction-guided synthesis of synchronization

Threesomes, with and without blame

Automatically generating instruction selectors using declarative machine descriptions

Modular verification of security protocol code by typing

Monads in action

Sequential verification of serializability

Program analysis via satisfiability modulo path programs

Verified just-in-time compiler on x86

Type inference for datalog with complex type hierarchies

A relational modal logic for higher-order stateful ADTs

Static determination of quantitative resource usage for higher-order programs

Structuring the verification of heap-manipulating programs

Modular session types for distributed object-oriented programming

Programming with angelic nondeterminism

Integrating typed and untyped code in a scripting language

Semantics and algorithms for data-dependent grammars

Dynamically checking ownership policies in concurrent c/c++ programs

Higher-order multi-parameter tree transducers and recursion schemes for program verification

Content Provider	ACM Digital Library
Author	Kobayashi, Naoki Unno, Hiroshi Tabuchi, Naoshi
Abstract	We introduce higher-order, multi-parameter, tree transducers (HMTTs, for short), which are kinds of higher-order tree transducers that take input trees and output a (possibly infinite) tree. We study the problem of checking whether the tree generated by a given HMTT conforms to a given output specification, provided that the input trees conform to input specifications (where both input/output specifications are regular tree languages). HMTTs subsume higher-order recursion schemes and ordinary tree transducers, so that their verification has a number of potential applications to verification of functional programs using recursive data structures, including resource usage verification, string analysis, and exact type-checking of XML-processing programs. We propose a sound but incomplete verification algorithm for the HMTT verification problem: the algorithm reduces the verification problem to a model-checking problem for higher-order recursion schemes extended with finite data domains, and then uses (an extension of)Kobayashi's algorithm for model-checking recursion schemes. While the algorithm is incomplete (indeed, as we show in the paper, the verification problem is undecidable in general), it is sound and complete for a subclass of HMTTs called linear HMTTs . We have applied our HMTT verification algorithm to various program verification problems and obtained promising results.
Starting Page	495
Ending Page	508
Page Count	14
File Format	PDF
ISBN	9781605584799
DOI	10.1145/1706299.1706355
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2010-01-17
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Higher-order tree transducers Higher-order recursion scheme Tree-processing programs Program verification
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

Higher-order multi-parameter tree transducers and recursion schemes for program verification

Types and higher-order recursion schemes for verification of higher-order programs

Untyped recursion schemes and infinite intersection types (2010)

Model-checking higher-order recursion schemes.

Types and higher-order recursion schemes for verification of higher-order programs (2009).

Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs (2009)

Types and higher-order recursion schemes for verification of higher-order programs

Model-checking higher-order functions

Io vs oi in higher-order recursion schemes axel (2013).

Higher-order multi-parameter tree transducers and recursion schemes for program verification

Similar Documents

Higher-order multi-parameter tree transducers and recursion schemes for program verification

Types and higher-order recursion schemes for verification of higher-order programs

Untyped recursion schemes and infinite intersection types (2010)

Model-checking higher-order recursion schemes.

Types and higher-order recursion schemes for verification of higher-order programs (2009).

Types and Higher-Order Recursion Schemes for Verification of Higher-Order Programs (2009)

Types and higher-order recursion schemes for verification of higher-order programs

Model-checking higher-order functions

Io vs oi in higher-order recursion schemes axel (2013).

Higher-order multi-parameter tree transducers and recursion schemes for program verification