NDLI: Automatic compositional reasoning for multi-thread programs

Content Provider	IEEE Xplore Digital Library
Author	Minqiang Gu Qiang Liu
Copyright Year	2011
Description	Author affiliation: School of Software, Tsinghua University, Beijing, 100084, China (Minqiang Gu; Qiang Liu)
Abstract	Automatic verification for multi-threaded programs has been an important and hard branch in model checking. The multi-thread programs are infinite systems which increase the state space with the number of the threads. To alleviate the state explosion, many techniques are proposed such as abstraction and compositional reasoning. However, the environment problem is the main barrier for the compositional reasoning. As a promising approach, thread modular consider the environment of the threads through shared variables, which is incomplete for the verification. In this paper, we will extend the thread modular reasoning to achieve complete compositional reasoning for multi-thread programs. We provide the automatic refinement strategy for the environment, which is generated by exposing necessary local information. And, we will combine the invariant deductive rule, reachability analysis and thread modular model reasoning for the verification of the multi-thread programs.
Starting Page	175
Ending Page	182
File Size	424288
Page Count	8
File Format	PDF
ISBN	9781457703867
e-ISBN	9781457703874
DOI	10.1109/CSCWD.2011.5960072
Language	English
Publisher	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Publisher Date	2011-06-08
Publisher Place	Switzerland
Access Restriction	Subscribed
Rights Holder	Institute of Electrical and Electronics Engineers, Inc. (IEEE)
Subject Keyword	Cognition Instruction sets Computational modeling Explosions Message systems Erbium Thread Modular Reasoning Model Checking Compositional Reasoning Multi-Thread
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

Automatic Compositional Reasoning for Probabilistic Model Checking of Hardware Designs

Reduction for compositional verification of multi-threaded programs

Interpolation Guided Compositional Verification (T)

Optimization towards Consolidation or Throughput for Multi-thread Software

Modeling and verifying context-aware non-monotonic reasoning agents

Scalable automatic linearizability checking

An Efficient Thread Recombining at Program Phase Changes

Learning Assumptions for CompositionalVerification of Timed Systems

Online Thread Assignment for Heterogeneous Multicore Systems

Automatic compositional reasoning for multi-thread programs

Similar Documents

Automatic Compositional Reasoning for Probabilistic Model Checking of Hardware Designs

Reduction for compositional verification of multi-threaded programs

Interpolation Guided Compositional Verification (T)

Optimization towards Consolidation or Throughput for Multi-thread Software

Modeling and verifying context-aware non-monotonic reasoning agents

Scalable automatic linearizability checking

An Efficient Thread Recombining at Program Phase Changes

Learning Assumptions for CompositionalVerification of Timed Systems

Online Thread Assignment for Heterogeneous Multicore Systems

Automatic compositional reasoning for multi-thread programs