scholarly journals GenMC: A Model Checker for Weak Memory Models

2021 ◽  
pp. 427-440
Author(s):  
Michalis Kokologiannakis ◽  
Viktor Vafeiadis
Keyword(s):  
Programming Languages ◽  
Error Detection ◽  
State Of The Art ◽  
Memory Models ◽  
Memory Model ◽  
Model Checker ◽  
C Programs ◽  
System Calls ◽  
Detection Capabilities ◽  
Additional Memory

AbstractGenMC is an LLVM-based state-of-the-art stateless model checker for concurrent C/C++ programs. Its modular infrastructure allows it to support complex memory models, such as RC11 and IMM, and makes it easy to extend to support further axiomatic memory models.In this paper, we discuss the overall architecture of the tool and how it can be extended to support additional memory models, programming languages, and/or synchronization primitives. To demonstrate the point, we have extended the tool with support for the Linux kernel memory model (LKMM), synchronization barriers, POSIX I/O system calls, and better error detection capabilities.

scholarly journals Dartagnan: Bounded Model Checking for Weak Memory Models (Competition Contribution)

2020 ◽  
pp. 378-382
Author(s):  
Hernán Ponce-de-León ◽  
Florian Furbach ◽  
Keijo Heljanko ◽  
Roland Meyer
Keyword(s):  
Model Checking ◽  
Bounded Model Checking ◽  
Memory Models ◽  
Memory Model ◽  
Complete Analysis ◽  
Concurrent Programs ◽  
Sequential Consistency ◽  
Model Checker ◽  
Safety Properties ◽  
C Programs

Abstract Dartagnanis a bounded model checker for concurrent programs under weak memory models. What makes it different from other tools is that the memory model is not hard-coded inside Dartagnanbut taken as part of the input. For SV-COMP’20, we take as input sequential consistency (i.e. the standard interleaving memory model) extended by support for atomic blocks. Our point is to demonstrate that a universal tool can be competitive and perform well in SV-COMP. Being a bounded model checker, Dartagnan’s focus is on disproving safety properties by finding counterexample executions. For programs with bounded loops, Dartagnanperforms an iterative unwinding that results in a complete analysis. The SV-COMP’20 version of Dartagnanworks on Boogiecode. The C programs of the competition are translated internally to Boogieusing SMACK.

scholarly journals Evaluation of the effectiveness and efficiency of state-of-the-art features and models for automatic speech recognition error detection

2021 ◽  
Vol 8 (1) ◽  
Author(s):  
Asmaa El Hannani ◽  
Rahhal Errattahi ◽  
Fatima Zahra Salmam ◽  
Thomas Hain ◽  
Hassan Ouahmane
Keyword(s):  
Speech Recognition ◽  
Automatic Speech Recognition ◽  
Error Detection ◽  
State Of The Art ◽  
Rapid Development ◽  
Unified Framework ◽  
Human Machine Interaction ◽  
Detection Analysis ◽  
Extensive Evaluation ◽  
Effectiveness And Efficiency

AbstractSpeech based human-machine interaction and natural language understanding applications have seen a rapid development and wide adoption over the last few decades. This has led to a proliferation of studies that investigate Error detection and classification in Automatic Speech Recognition (ASR) systems. However, different data sets and evaluation protocols are used, making direct comparisons of the proposed approaches (e.g. features and models) difficult. In this paper we perform an extensive evaluation of the effectiveness and efficiency of state-of-the-art approaches in a unified framework for both errors detection and errors type classification. We make three primary contributions throughout this paper: (1) we have compared our Variant Recurrent Neural Network (V-RNN) model with three other state-of-the-art neural based models, and have shown that the V-RNN model is the most effective classifier for ASR error detection in term of accuracy and speed, (2) we have compared four features’ settings, corresponding to different categories of predictor features and have shown that the generic features are particularly suitable for real-time ASR error detection applications, and (3) we have looked at the post generalization ability of our error detection framework and performed a detailed post detection analysis in order to perceive the recognition errors that are difficult to detect.

Employing Space-Based Hyperspectral Imagery for Pipeline Leak Prevention, Detection and Compliance

2020 ◽  
Author(s):  
R. Peter Weaver ◽  
Dan Katz ◽  
Tushar Prabahakar ◽  
Katie A. Corcoran
Keyword(s):  
Environmental Protection Agency ◽  
Oil And Gas ◽  
State Of The Art ◽  
Hyperspectral Imagery ◽  
Cost Effective ◽  
Protection Agency ◽  
High Resolution Data ◽  
Hydrocarbon Detection ◽  
Detection Capabilities ◽  
Vapor Emissions

Abstract We are now living in what has been described as the Experience Era, where lines between the digital and physical are increasingly blurred. As such, we are just beginning to see how customized access to space will improve asset stewardship in ways that are still evolving, as customization of on-orbit technology pushes the bounds of how we receive and process information. Specific to oil and gas operators, one technology being launched by microsatellite, hyperspectral imagery (HSI), is poised to enable unparalleled daily global pipeline leak prevention, detection and speciation, intrusion and change detection capabilities. This will replace conventional DOT pipeline patrol for compliance while contributing to our understanding of vapor emissions as regulated by the Environmental Protection Agency. This paper discusses both the evolving space marketplace and the state of the art for HSI, including current examples of hyperspectral findings regarding pipeline and terminal leaks. Successful deployment of HSI will drive a decrease in the number and magnitude of pipeline leaks using persistent, global, high-resolution data collection, rapid and reliable analysis, and immediate reporting of actionable information. For decades, satellite HSI technology has offered a promise of remote hydrocarbon detection and other features of interest. It is only now becoming scalable, accessible to, and cost-effective for the pipeline industry, and thus a reality for cost-effective pipeline stewardship.

Performance Characteristics of Several Rules for Self-interpretation of Proficiency Testing Data

2005 ◽  
Vol 129 (8) ◽  
pp. 997-1003 ◽  
Author(s):  
R. Neill Carey ◽  
George S. Cembrowski ◽  
Carl C. Garber ◽  
Zohreh Zaki
Keyword(s):  
Proficiency Testing ◽  
Error Detection ◽  
Clinical Laboratory ◽  
Peer Group ◽  
Simulation Techniques ◽  
Allowable Error ◽  
Detection Capabilities ◽  
The Mean ◽  
The Difference

Abstract Context.—Proficiency testing (PT) participants can interpret their results to detect errors even when their performance is acceptable according to the limits set by the PT provider. Objective.—To determine which rules for interpreting PT data provide optimal performance for PT with 5 samples per event. Design.—We used Monte Carlo computer simulation techniques to study the performance of several rules, relating their error detection capabilities to (1) the analytic quality of the method, (2) the probability of failing PT, and (3) the ratio of the peer group SD to the mean intralaboratory SD. Analytic quality is indicated by the ratio of the PT allowable error to the intralaboratory SD. Failure of PT was defined (Clinical Laboratory Improvement Amendments of 1988) as an event when 2 or more results out of 5 exceeded acceptable limits. We investigated rules with limits based on the SD index, the mean SD index, and percentages of allowable error. Results.—No single rule performs optimally across the range of method quality. Conclusions.—We recommend further investigation when PT data cause rejection by any of the following 3 rules: any result exceeds 75% of allowable error, the difference between any 2 results exceeds 4 times the peer group SD, or the mean SD index of all 5 results exceeds 1.5. As method quality increases from marginal to high, false rejections range from 16% to nearly zero, and the probability of detecting a shift equal to 2 times the intralaboratory SD ranges from 94% to 69%.

An Enhanced Dynamic Information Flow Tracking Method with Reverse Stack Execution

2015 ◽  
Vol 3 (1) ◽  
pp. 40-58 ◽  
Author(s):  
Anna Trikalinou ◽  
Nikolaos Bourbakis
Keyword(s):  
Programming Languages ◽  
Information Flow ◽  
Attack Detection ◽  
Control Flow ◽  
Security Issue ◽  
Memory Errors ◽  
Dynamic Information ◽  
C Programs ◽  
Information Flow Tracking ◽  
Dynamic Information Flow Tracking

Memory errors have long been a critical security issue primarily for C/C++ programming languages and are still considered one of the top three most dangerous software errors according to the MITRE ranking. In this paper the authors focus on their exploitation via control-flow hijacking and data-only attacks (stack, and partially heap (G. Novarck & E. Berger, 2010)) by proposing a synergistic security methodology, which can accurately detect and thwart them. Their methodology is based on the Dynamic Information Flow Tracking (DIFT) technique and improves its data-only attack detection by utilizing features from the Reverse Stack Execution (RSE) security technique. Thus, the authors can significantly lower the resource consumption of the latter methodology, while increasing the former's accuracy. Their proof-of-concept compiler implementation verifies their assumptions and is able to protect vulnerable C programs against various real-world attack scenarios.

scholarly journals αCheck: A mechanized metatheory model checker

2017 ◽  
Vol 17 (3) ◽  
pp. 311-352 ◽  
Author(s):  
JAMES CHENEY ◽  
ALBERTO MOMIGLIANO
Keyword(s):  
Programming Language ◽  
Dual Problem ◽  
State Of The Art ◽  
Operational Semantics ◽  
Type Systems ◽  
Model Checker ◽  
Formal Systems ◽  
Current State ◽  
Fully Automatic ◽  
Nominal Logic

AbstractThe problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has received considerable attention recently. However, the dual problem of searching for errors in such formalizations has attracted comparatively little attention. In this article, we present αCheck, a bounded model checker for metatheoretic properties of formal systems specified using nominal logic. In contrast to the current state of the art for metatheory verification, our approach is fully automatic, does not require expertise in theorem proving on the part of the user, and produces counterexamples in the case that a flaw is detected. We present two implementations of this technique, one based onnegation-as-failureand one based onnegation elimination, along with experimental results showing that these techniques are fast enough to be used interactively to debug systems as they are developed.

Interpretive MPI for Parallel Computing

2008 ◽  
Author(s):  
Yu-Cheng Chou ◽  
Harry H. Cheng
Keyword(s):  
Parallel Computing ◽  
Programming Languages ◽  
Message Passing ◽  
Large Scale ◽  
Message Passing Interface ◽  
Rapid Development ◽  
Web Based ◽  
Heterogeneous Platforms ◽  
C Programs ◽  
Computation Speedup

Message Passing Interface (MPI) is a standardized library specification designed for message-passing parallel programming on large-scale distributed systems. A number of MPI libraries have been implemented to allow users to develop portable programs using the scientific programming languages, Fortran, C and C++. Ch is an embeddable C/C++ interpreter that provides an interpretive environment for C/C++ based scripts and programs. Combining Ch with any MPI C/C++ library provides the functionality for rapid development of MPI C/C++ programs without compilation. In this article, the method of interfacing Ch scripts with MPI C implementations is introduced by using the MPICH2 C library as an example. The MPICH2-based Ch MPI package provides users with the ability to interpretively run MPI C program based on the MPICH2 C library. Running MPI programs through the MPICH2-based Ch MPI package across heterogeneous platforms consisting of Linux and Windows machines is illustrated. Comparisons for the bandwidth, latency, and parallel computation speedup between C MPI, Ch MPI, and MPI for Python in an Ethernet-based environment comprising identical Linux machines are presented. A Web-based example is given to demonstrate the use of Ch and MPICH2 in C based CGI scripting to facilitate the development of Web-based applications for parallel computing.

Sign in / Sign up

Export Citation Format

Share Document