NDLI: Analysis of invariants for efficient bounded verification

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

Proving memory safety of floating-point computations by combining static and dynamic program analysis

Directed test generation for effective fault localization

Generating test cases for specification mining

Automatic detection of unsafe component loadings

Automated analysis of load testing results

Mutation-driven generation of unit tests and oracles

Parallel symbolic execution for structural test generation

Formal analysis of the effectiveness and predictability of random testing

Analyzing concurrency bugs using dual slicing

Software fault prediction tool

Strict control dependence and its effect on dynamic information flow analyses

Automated fixing of programs with contracts

Modeling consumer-perceived web application fault severities for testing

Learning from 6,000 projects: lightweight cross-project anomaly detection

OCAT: object capture-based automated testing

Exploiting program dependencies for scalable multiple-path symbolic execution

A study on agility and testing processes in software organizations

N-version disassembly: differential testing of x86 disassemblers

ASSURE: automated support for secure and usable requirements engineering

Analysis of invariants for efficient bounded verification

Causal inference for statistical fault localization

Perturbing numerical calculations for statistical analysis of floating-point program (in)stability

Testing system virtual machines

On test repair using symbolic execution

The Google FindBugs fixit

Automatically identifying critical input regions and code in applications

Analysis of invariants for efficient bounded verification

Content Provider	ACM Digital Library
Author	López Pombo, Carlos Gustavo Frias, Marcelo Fabian Rosner, Nicolás Galeotti, Juan Pablo
Abstract	SAT-based bounded verification of annotated code consists of translating the code together with the annotations to a propositional formula, and analyzing the formula for specification violations using a SAT-solver. If a violation is found, an execution trace exposing the error is exhibited. Code involving linked data structures with intricate invariants is particularly hard to analyze using these techniques. In this article we present TACO, a prototype tool which implements a novel, general and fully automated technique for the SAT-based analysis of JML-annotated Java sequential programs dealing with complex linked data structures. We instrument code analysis with a symmetry-breaking predicate that allows for the parallel, automated computation of tight bounds for Java fields. Experiments show that the translations to propositional formulas require significantly less propositional variables, leading in the experiments we have carried out to an improvement on the efficiency of the analysis of orders of magnitude, compared to the non-instrumented SAT-based analysis. We show that, in some cases, our tool can uncover bugs that cannot be detected by state-of-the-art tools based on SAT-solving, model checking or SMT-solving.
Starting Page	25
Ending Page	36
Page Count	12
File Format	PDF
ISBN	9781605588230
DOI	10.1145/1831708.1831712
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2010-07-12
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Dynalloy Kodkod Sat-based code analysis Static analysis Alloy
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

TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds

Parallel bounded analysis in code with rich invariants by refinement of field bounds

Efficient SAT-based bounded model checking for software verification (2004)

A dataflow analysis to improve sat-based bounded program verification.

Modular verification of code with SAT

Bounded exhaustive test input generation from hybrid invariants

Generating runtime verification specifications based on static code analysis alerts

SAT-based verification of safe Petri nets

A SAT-based Method for Basis Path Testing using KodKod

Analysis of invariants for efficient bounded verification

Similar Documents

TACO: Efficient SAT-Based Bounded Verification Using Symmetry Breaking and Tight Bounds

Parallel bounded analysis in code with rich invariants by refinement of field bounds

Efficient SAT-based bounded model checking for software verification (2004)

A dataflow analysis to improve sat-based bounded program verification.

Modular verification of code with SAT

Bounded exhaustive test input generation from hybrid invariants

Generating runtime verification specifications based on static code analysis alerts

SAT-based verification of safe Petri nets

A SAT-based Method for Basis Path Testing using KodKod

Analysis of invariants for efficient bounded verification