NDLI: Conditional model checking: a technique to pass information between verifiers

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

ACM SIGSOFT Impact Paper Award 2012: Systematic Software Testing: The Korat Approach

Testing mined specifications

SelfMotion: a declarative language for adaptive service-oriented mobile apps

Searching connected API subgraph via text phrases

Practical change impact analysis based on static program slicing for industrial software systems

Automating presentation changes in dynamic web applications via collaborative hybrid analysis

SecuriTAS: a tool for engineering adaptive security

Dealing with uncertainty in early software architecture

Understanding myths and realities of test-suite evolution

UMLtoCSP (UOST): a tool for efficient verification of UML/OCL class diagrams through model slicing

Improving software developers' fluency by recommending development environment commands

DTAM: dynamic taint analysis of multi-threaded programs for relevancy

Do crosscutting concerns cause modularity problems?

A case study of cross-system porting in forked projects

Conditional model checking: a technique to pass information between verifiers

Recalling the "imprecision" of cross-project defect prediction

Detecting and analyzing insecure component usage

REPERTOIRE: a cross-system porting analysis tool for forked software projects

AUSUM: approach for unsupervised bug report summarization

MayPar: a may-happen-in-parallel analyzer for concurrent objects

Mining the execution history of a software system to infer the best time for its adaptation

Dione: an integrated measurement and defect prediction solution

Software change contracts

Test input generation using dynamic programming

ReImInfer: method purity inference for Java

History slicing: assisting code-evolution tasks

Predicting null-pointer dereferences in concurrent programs

A field study of refactoring challenges and benefits

How do developers use parallel libraries?

Green: reducing, reusing and recycling constraints in program analysis

An industrial study on the risk of software changes

Retargeting Android applications to Java bytecode

Automating adaptive maintenance changes with SrcML and LINQ

Automated extraction of security policies from natural-language software documents

Sando: an extensible local code search framework

Semantic fault diagnosis: automatic natural-language fault descriptions

CarFast: achieving higher statement coverage faster

TouchDevelop: app development on mobile devices

Who is going to mentor newcomers in open source projects?

Asynchronous programs with prioritized task-buffers

How do software engineers understand code changes?: an exploratory study in industry

Seeking the ground truth: a retroactive study on the evolution and migration of software libraries

Automated concolic testing of smartphone apps

Multi-layered approach for recovering links between bug reports and fixes

Toward measuring program comprehension with functional magnetic resonance imaging

Scalable test data generation from multidimensional models

FaultTracer: a change impact and regression fault analysis tool for evolving Java programs

Assessing the value of branches with what-if analysis

Variability points and design pattern usage in architectural tactics

How do developers react to API deprecation?: the case of a smalltalk ecosystem

Rubicon: bounded verification of web applications

Toward semantic search via SMT solver

Efficiently scripting change-resilient tests

Inference and checking of context-sensitive pluggable types

Scalable malware clustering through coarse-grained behavior modeling

Has this bug been reported?

Concept-based failure clustering

Seeing the forest and the trees: focusing team interaction on value and effort drivers

From pixels to bytes: evolutionary scenario based design with video

Service selection for happy users: making user-intuitive quality abstractions

Conditional model checking: a technique to pass information between verifiers

Content Provider	ACM Digital Library
Author	Keremoglu, M. Erkan Beyer, Dirk Wendler, Philipp Henzinger, Thomas A.
Abstract	Software model checking, as an undecidable problem, has three possible outcomes: (1) the program satisfies the specification, (2) the program does not satisfy the specification, and (3) the model checker fails. The third outcome usually manifests itself in a space-out, time-out, or one component of the verification tool giving up; in all of these failing cases, significant computation is performed by the verification tool before the failure, but no result is reported. We propose to reformulate the model-checking problem as follows, in order to have the verification tool report a summary of the performed work even in case of failure: given a program and a specification, the model checker returns a condition Ψ ---usually a state predicate--- such that the program satisfies the specification under the condition Ψ ---that is, as long as the program does not leave the states in which Ψ is satisfied. In our experiments, we investigated as one major application of conditional model checking the sequential combination of model checkers with information passing. We give the condition that one model checker produces, as input to a second conditional model checker, such that the verification problem for the second is restricted to the part of the state space that is not covered by the condition, i.e., the second model checker works on the problems that the first model checker could not solve. Our experiments demonstrate that repeated application of conditional model checkers, passing information from one model checker to the next, can significantly improve the verification results and performance, i.e., we can now verify programs that we could not verify before.
Starting Page	1
Ending Page	11
Page Count	11
File Format	PDF
ISBN	9781450316149
DOI	10.1145/2393596.2393664
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2012-11-11
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	Sequential combination Model checking Coverage Program analysis Formal verification Testing
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