NDLI: Approximating happens-before order: interplay between static analysis and state space traversal

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

Approximating happens-before order: interplay between static analysis and state space traversal

Automatic handling of native methods in Java PathFinder

Local state space construction for compositional verification of concurrent systems

CTL+FO verification as constraint solving

Exploiting synchronization in the analysis of shared-memory asynchronous programs

Quantifying information leaks using reliability analysis

Certification for configurable program analysis

Toward parameterized verification of synchronous distributed applications

Incremental bounded software model checking

Towards a test automation framework for alloy

An improvement of the piggyback algorithm for parallel model checking

SpinCause: a tool for causality checking

Satisfiability modulo abstraction for separation logic with linked lists

Verige: verification with invariant generation engine

Is there a best büchi automaton for explicit model checking?

SpinRCP: the eclipse rich client platform integrated development environment for the spin model checker

Generic and efficient attacker models in SPIN

TravMC2: higher-order model checking for alternating parity tree automata

Towards a GPGPU-parallel SPIN model checker

Unit testing for SPIN: runspin and parsepan

Approximating happens-before order: interplay between static analysis and state space traversal

Content Provider	ACM Digital Library
Author	Jančík, Pavel Parízek, Pavel
Abstract	Techniques and tools for verification of multi-threaded programs must cope with the huge number of possible thread interleavings. Tools based on systematic exploration of a program state space employ partial order reduction to avoid redundant thread interleavings. The key idea is to make non-deterministic thread scheduling choices only at statements that read or modify the global state shared by multiple threads. We focus on the approach to partial order reduction used in tools such as Java Pathfinder (JPF), which construct the program state space on-the-fly, and therefore can use only information available in the current program state and execution history to identify statements that may be globally-relevant. In our previous work, we developed a field access analysis that provides information about fields that may be accessed during program execution, and used it in JPF for more precise identification of globally-relevant statements. We build upon that and propose a may-happen-before analysis that computes a sound approximation of the happens-before ordering. Partial order reduction techniques can use the happens-before ordering to detect pairs of globally-relevant field access statements that cannot be interleaved arbitrarily (due to thread synchronization), and based on that avoid making unnecessary thread scheduling choices. The may-happen-before analysis combines static analysis with knowledge of information available from the dynamic program state. Results of experiments with several Java programs show that usage of the may-happen-before analysis further improves the performance of JPF. .
Starting Page	1
Ending Page	10
Page Count	10
File Format	PDF
ISBN	9781450324526
DOI	10.1145/2632362.2632365
Language	English
Publisher	Association for Computing Machinery (ACM)
Publisher Date	2014-07-21
Publisher Place	New York
Access Restriction	Subscribed
Subject Keyword	State space traversal Java pathfinder Concurrency Dynamic analysis Static analysis Happens-before
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