NDLI: Higher-order test generation

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

Commutative set: a language extension for implicit parallel programming

Data representation synthesis

Generalized just-in-time trace compilation using a parallel task farm in a dynamic binary translator

Caisson: a hardware description language for secure information flow

Automatic CPU-GPU communication management and optimization

Understanding POWER multiprocessors

Probabilistic, modular and scalable inference of typestate specifications

Toward generating reducible replay logs

Finding and understanding bugs in C compilers

Spreadsheet table transformations from examples

A security policy oracle: detecting security holes using multiple API implementations

Isolating and understanding concurrency errors using reconstructed execution fragments

Garbage collection for monitoring parametric properties

Cause clue clauses: error localization using maximum satisfiability

Kremlin: rethinking and rebooting gprof for the multicore age

Path-based inductive synthesis for program inversion

Verification of semantic commutativity conditions and inverse operations on linked data structures

Precise and compact modular procedure summaries for heap manipulating programs

Taming the wildcards: combining definition- and use-site variance

Composable asynchronous events

The tao of parallelism in algorithms

Synthesizing geometry constructions

Brainy: effective selection of data structures

Steno: automatic optimization of declarative queries

Automatic compilation of MATLAB programs for synergistic execution on heterogeneous processors

Partial-coherence abstractions for relaxed memory models

Predicate abstraction and CEGAR for higher-order model checking

Higher-order test generation

Evaluating value-graph translation validation for LLVM

Systematic editing: generating program transformations from an example

Language-independent sandboxing of just-in-time compilation and self-modifying code

Automated atomicity-violation fixing

LL(*): the foundation of the ANTLR parser generator

kb-anonymity: a model for anonymized behaviour-preserving test and debugging data

Automatic parallelization via matrix multiplication

Directed incremental symbolic execution

Exploiting the commutativity lattice

On inter-procedural analysis of programs with lists and data

Taming wildcards in Java's type system

Synchronization via scheduling: techniques for efficiently managing shared state

Parallelism orchestration using DoPE: the degree of parallelism executive

Synthesis of loop-free programs

An SSA-based algorithm for optimal speculative code motion under an execution profile

Languages as libraries

EnerJ: approximate data types for safe and general low-power computation

A case for an SC-preserving compiler

Mostly-automated verification of low-level programs in computational separation logic

LeakChaser: helping programmers narrow down causes of memory leaks

Safe optimisations for shared-memory concurrent programs

Cruiser: concurrent heap buffer overflow monitoring using lock-free data structures

NDSeq: runtime checking for nondeterministic sequential specifications of parallel correctness

ALTER: exploiting breakable dependences for parallelization

Mining hot calling contexts in small space

Separation logic + superposition calculus = heap theorem prover

Scaling abstraction refinement via pruning

Higher-order test generation

Content Provider	ACM Digital Library
Author	Godefroid, Patrice
Abstract	Symbolic reasoning about large programs is bound to be imprecise. How to deal with this imprecision is a fundamental problem in program analysis. Imprecision forces approximation. Traditional static program verification builds "may" over-approximations of the program behaviors to check universal "for-all-paths" properties, while automatic test generation requires "must" under-approximations to check existential "for-some-path" properties. In this paper, we introduce a new approach to test generation where tests are derived from validity proofs of first-order logic formulas, rather than satisfying assignments of quantifier-free first-order logic formulas as usual. Two key ingredients of this higher-order test generation are to (1) represent complex/unknown program functions/instructions causing imprecision in symbolic execution by uninterpreted functions, and (2) record uninterpreted function samples capturing input-output pairs observed at execution time for those functions. We show that higher-order test generation generalizes and is more precise than simplifying complex symbolic expressions using their concrete runtime values. We present several program examples where our approach can exercise program paths and find bugs missed by previous techniques. We discuss the implementability and applications of this approach. We also explain in what sense dynamic test generation is more powerful than static test generation.
Starting Page	258
Ending Page	269
Page Count	12
File Format	PDF
ISBN	9781450306638
DOI	10.1145/1993498.1993529
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2011-06-04
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Uninterpreted functions Software model checking Automatic test generation
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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