scholarly journals Case Studies on Invariant Generation Using a Saturation Theorem Prover

2011 ◽  
pp. 1-15 ◽  
Author(s):  
Kryštof Hoder ◽  
Laura Kovács ◽  
Andrei Voronkov
Keyword(s):  
Case Studies ◽  
Theorem Prover ◽  
Invariant Generation ◽  
Saturation Theorem

scholarly journals Invariants and Robustness of BIP Models

10.29007/prxp ◽  
2018 ◽  
Author(s):  
Jan Olaf Blech ◽  
Thanh-Hung Nguyen ◽  
Michael Perin
Keyword(s):  
Embedded Systems ◽  
Higher Order ◽  
Theorem Prover ◽  
Important Goal ◽  
Invariant Generation ◽  
Execution Traces ◽  
Verification Tool ◽  
Verification Tools ◽  
Generation Mechanisms ◽  
Natural Way

In this paper we present on-going work addressing the problem of automatically generating realistic and guaranteed correct invariants. Since invariant generation mechanisms are error-prone, after the computation of invariants by a verification tool, we formally prove that the generated invariants are indeed invariants of the considered systems using a higher-order theorem prover and automated techniques. We regard invariants for BIP models. BIP (behavior, interaction, priority) is a language for specifying asynchronous component based systems. Proving that an invariant holds often requires an induction on possible system execution traces. For this reason, apart from generating invariants that precisely capture a system’s behavior, inductiveness of invariants is an important goal. We establish a notion of robust BIP models. These can be automatically constructed from our original non-robust BIP models and over-approximate their behavior. We motivate that invariants of robust BIP models capture the behavior of systems in a more natural way than invariants of corresponding non-robust BIP models. Robust BIP models take imprecision due to values delivered by sensors into account. Invariants of robust BIP models tend to be inductive and are also invariants of the original non-robust BIP model. Therefore they may be used by our verification tools and it is easy to show their correctness in a higher-order theorem prover. The presented work is developed to verify the results of a deadlock-checking tool for embedded systems after their computations. Therewith, we gain confidence in the provided analysis results.

scholarly journals Reasoning About Loops Using Vampire

10.29007/tcvj ◽  
2018 ◽  
Author(s):  
Laura Kovács ◽  
Simon Robillard
Keyword(s):  
Order Logic ◽  
Theorem Prover ◽  
Program Correctness ◽  
Command Language ◽  
Rule Based ◽  
Invariant Generation ◽  
Partial Correctness ◽  
First Order ◽  
Deductive Systems ◽  
Fully Automatic

In 2009, the symbol elimination method for loop invariant generationwas introduced, which used saturationtheorem proving in first-order logic to generate quantified invariantsof programs with arrays. Symbol elimination is fully automatic,requires no user guidance, and it is the first ever approach able togenerate invariants with alternations of quantifiers. In this paperwe describe a number of improvements and extensions to symbolelimination and invariant generation using first-order theoremproving, in particular the Vampire theorem prover. Rather than beinglimited to a specific programming language, our approach to reasoningabout loops in Vampire relies on a simple guarded command language forits input, which can be used as an interface for more complex andrealistic imperative languages. We propose new ways for extendingquantified loop properties describing valid loop properties, bysimplifying the properties over array updates and next staterelations. We also extend symbol elimination with pre- andpost-conditions of loops. We use the loop specification to generateonly invariants that are relevant, that is, invariants that are neededfor proving partial correctness of loops. Further, we turn symbolelimination into an automatic approach proving program correctness,providing an alternative method to Hoare-rule based loop verificationor other deductive systems. We present our newly redesignedimplementation of loop reasoning in Vampire and also report onexperimental results.

scholarly journals Pegasus: sound continuous invariant generation

2021 ◽  
Author(s):  
Andrew Sogokon ◽  
Stefan Mitsch ◽  
Yong Kiam Tan ◽  
Katherine Cordwell ◽  
André Platzer
Keyword(s):  
Hybrid Systems ◽  
Experimental Evaluation ◽  
Discrete Systems ◽  
Automatic Generation ◽  
Theorem Prover ◽  
Continuous Systems ◽  
Formal Proofs ◽  
Deductive Verification ◽  
Invariant Generation ◽  
Discrete Invariants

AbstractContinuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without having to unroll their loops, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.

Corporate Sustainability: Challenge to Managerial Orthodoxies

2003 ◽  
Vol 9 (1) ◽  
pp. 2-11 ◽  
Author(s):  
Dexter Dunphy
Keyword(s):  
Case Studies ◽  
Corporate Sustainability ◽  
Central Place ◽  
Marked Contrast ◽  
Sustainability Management

ABSTRACTThis paper addresses the issue of corporate sustainability. It examines why achieving sustainability is becoming an increasingly vital issue for society and organisations, defines sustainability and then outlines a set of phases through which organisations can move to achieve increasing levels of sustainability. Case studies are presented of organisations at various phases indicating the benefits, for the organisation and its stakeholders, which can be made at each phase. Finally the paper argues that there is a marked contrast between the two competing philosophies of neo-conservatism (economic rationalism) and the emerging philosophy of sustainability. Management schools have been strongly influenced by economic rationalism, which underpins the traditional orthodoxies presented in such schools. Sustainability represents an urgent challenge for management schools to rethink these traditional orthodoxies and give sustainability a central place in the curriculum.

Short-Form Application of the Screening Test of Spanish Grammar and the Northwestern Syntax Screening Test to Latino Children

1978 ◽  
Vol 9 (4) ◽  
pp. 220-235
Author(s):  
David L. Ratusnik ◽  
Carol Melnick Ratusnik ◽  
Karen Sattinger
Keyword(s):  
New York ◽  
Case Studies ◽  
Metropolitan Area ◽  
Screening Test ◽  
Normative Data ◽  
Short Form ◽  
Latino Children ◽  
Data Application ◽  
York Metropolitan Area ◽  
Multiple Regression Technique

Short-form versions of the Screening Test of Spanish Grammar (Toronto, 1973) and the Northwestern Syntax Screening Test (Lee, 1971) were devised for use with bilingual Latino children while preserving the original normative data. Application of a multiple regression technique to data collected on 60 lower social status Latino children (four years and six months to seven years and one month) from Spanish Harlem and Yonkers, New York, yielded a small but powerful set of predictor items from the Spanish and English tests. Clinicians may make rapid and accurate predictions of STSG or NSST total screening scores from administration of substantially shortened versions of the instruments. Case studies of Latino children from Chicago and Miami serve to cross-validate the procedure outside the New York metropolitan area.

Case Studies for Telepractice in AAC

2014 ◽  
Vol 23 (1) ◽  
pp. 42-54 ◽  
Author(s):  
Tanya Rose Curtis
Keyword(s):  
Service Delivery ◽  
Case Studies ◽  
Eye Gaze ◽  
Cognitive Impairments ◽  
Perceived Barriers ◽  
Computer Experience ◽  
Access Methods ◽  
Complex Communication Needs ◽  
Barriers To Service ◽  
Communication Needs

As the field of telepractice grows, perceived barriers to service delivery must be anticipated and addressed in order to provide appropriate service delivery to individuals who will benefit from this model. When applying telepractice to the field of AAC, additional barriers are encountered when clients with complex communication needs are unable to speak, often present with severe quadriplegia and are unable to position themselves or access the computer independently, and/or may have cognitive impairments and limited computer experience. Some access methods, such as eye gaze, can also present technological challenges in the telepractice environment. These barriers can be overcome, and telepractice is not only practical and effective, but often a preferred means of service delivery for persons with complex communication needs.

What Makes for Effective Online Treatment?

ASHA Leader ◽  
2013 ◽  
Vol 18 (1) ◽  
pp. 12-13
Author(s):  
Kristen Chmela
Keyword(s):  
Case Studies ◽  
Executive Director ◽  
Fluency Disorders ◽  
Online Treatment

In November, Kristen Chmela—executive director of the Chmela Fluency Center in Long Grove, Ill.—chatted with participants from ASHA’s online conference, Case Studies in Fluency Disorders. The Leader listened in.

Sign in / Sign up

Export Citation Format

Share Document