NDLI: Enhancing symbolic execution with built-in term rewriting and constrained lazy initialization

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

A logical revolution (keynote)

Empirical answers to fundamental software engineering problems (panel)

Artifact evaluation (summary)

Efficiency and early fault detection with lower and higher strength combinatorial interaction testing

Adequate monitoring of service compositions

Bayesian inference using data flow analysis

An empirical analysis of the co-evolution of schema and code in database applications

Finding incorrect compositions of atomicity

Will you still compile me tomorrow? static cross-version compiler validation

Dynodroid: an input generation system for Android apps

SPLat: lightweight dynamic analysis for reducing combinatorics in testing configurable systems

Feature model extraction from large collections of informal product descriptions

Making offline analyses continuous

Preventing database deadlocks in applications

Precision reuse for efficient regression verification

Mining behavior models from enterprise web applications

Searching for better configurations: a rigorous approach to clone evaluation

Jalangi: a selective record-replay and dynamic analysis framework for JavaScript

Explaining inconsistent code

Scalable and incremental software bug detection

SocialCDE: a social awareness tool for global software teams

RUBRIC: a flexible tool for automated checking of conformance to requirement boilerplates

Jalangi: a tool framework for concolic testing, selective record-replay, and dynamic analysis of JavaScript

Extracting URLs from JavaScript via program analysis

A cost-effectiveness criterion for applying software defect prediction models

Understanding gamification mechanisms for software development

Precise range analysis on large industry code

ShAir: extensible middleware for mobile peer-to-peer resource sharing

h-ubu: an industrial-strength service-oriented component framework for JavaScript applications

Automatically describing software faults

PHRT: a model and programmable tool for hardware reengineering automation

Automotive architecture description and its quality

A framework for defining the dynamic semantics of DSLs

Producing software by integration: challenges and research directions (keynote)

A publication culture in software engineering (panel)

Con2colic testing

Prediction of atomic web services reliability based on k-means clustering

Second-order constraints in dynamic invariant inference

Automated oracles: an empirical study on cost and effectiveness

Tightfit: adaptive parallelization with foresight

Convergent contemporary software peer review practices

KATCH: high-coverage testing of software patches

Cachetor: detecting cacheable data to remove bloat

N-way model merging

Regression tests to expose change interaction errors

Identifying message flow in distributed event-based systems

Cascading verification: an integrated method for domain-specific model checking

Incrementally synthesizing controllers from scenario-based product line specifications

Diversity in software engineering research

Practical static analysis of JavaScript applications in the presence of frameworks and libraries

A statistical semantic language model for source code

Inferring project-specific bug patterns for detecting sibling bugs

REDACT: preventing database deadlocks from application-based transactions

RiTHM: a tool for enabling time-triggered runtime verification for C programs

RSA-MBT: a test tool for generating test artifacts based on models

Data debugging with continuous testing

BugMap: a topographic map of bugs

Toward understanding the causes of unanswered questions in software information sites: a case study of stack overflow

Agreements for software reuse in corporations

Risky files: an approach to focus quality improvement effort

Design and optimization of multi-clocked embedded systems using formal technique

Fuzzy service matching in on-the-fly computing

Using topic models to understand the evolution of a software ecosystem

Towards open architecture system

Software engineering for mathematics (keynote)

Boosting concolic testing via interpolation

Scalable analysis of variable software

Z3-str: a z3-based string solver for web application analysis

Sample size vs. bias in defect prediction

Distributed program tracing

Do all task dependencies require coordination? the role of task properties in identifying critical coordination needs in software projects

Termination proofs from tests

Effective dynamic detection of alias analysis errors

Compiling mockups to flexible UIs

Differential assertion checking

Improving trace accuracy through data-driven configuration and composition of tracing features

Enhancing symbolic execution with built-in term rewriting and constrained lazy initialization

Synthesis of component and connector models from crosscutting structural views

API change and fault proneness: a threat to the success of Android apps

Server interface descriptions for automated testing of JavaScript web applications

Crossing the gap from imperative to functional programming through refactoring

Mining succinct predicated bug signatures

aPET: a test case generation tool for concurrent objects

PoMMaDe: pushdown model-checking for malware detection

USMMC: a self-contained model checker for UML state machines

Iterative test suites refinement for elastic computing systems

Lexical statistical machine translation for language migration

Where is the business logic?

Good technology makes the difficult task easy

System reliability calculation based on the run-time analysis of ladder program

The economics of static analysis tools

RADA: a tool for reasoning about algebraic data types with abstractions

Using fault history to improve mutation reduction

Code fragment summarization

Towards emotional awareness in software development teams

Enhancing symbolic execution with built-in term rewriting and constrained lazy initialization

Content Provider	ACM Digital Library
Author	Pezzè, Mauro Braione, Pietro Denaro, Giovanni
Abstract	Symbolic execution suffers from problems when analyzing programs that handle complex data structures as their inputs and take decisions over non-linear expressions. For these programs, symbolic execution may incur invalid inputs or unidentified infeasible traces, and may raise large amounts of false alarms. Some symbolic executors tackle these problems by introducing executable preconditions to exclude invalid inputs, and some solvers exploit rewrite rules to address non linear problems. In this paper, we discuss the core limitations of executable preconditions, and address these limitations by proposing invariants specifically designed to harmonize with the lazy initialization algorithm. We exploit rewrite rules applied within the symbolic executor, to address simplifications of inverse relationships fostered from either program-specific calculations or the logic of the verification tasks. We present a symbolic executor that integrates the two techniques, and validate our approach against the verification of a relevant set of properties of the Tactical Separation Assisted Flight Environment. The empirical data show that the integrated approach can improve the effectiveness of symbolic execution. .
Starting Page	411
Ending Page	421
Page Count	11
File Format	PDF
ISBN	9781450322379
DOI	10.1145/2491411.2491433
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2013-08-18
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Software analysis Symbolic execution
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