Tool Support for Logics of Programs

1997 ◽  
pp. 461-498
Author(s):  
Lawrence C. Paulson
Keyword(s):  
Tool Support ◽  
Logics Of Programs

scholarly journals Reasoning with the HERMIT: tool support for equational reasoning on GHC core programs

2016 ◽  
Vol 50 (12) ◽  
pp. 23-34 ◽  
Author(s):  
Andrew Farmer ◽  
Neil Sculthorpe ◽  
Andy Gill
Keyword(s):  
Tool Support ◽  
Equational Reasoning

scholarly journals Correct program parallelisations

2021 ◽  
Author(s):  
S. Blom ◽  
S. Darabi ◽  
M. Huisman ◽  
M. Safari
Keyword(s):  
Composition Operators ◽  
Parallel Programs ◽  
Parallel Program ◽  
Tool Support ◽  
Intermediate Representation ◽  
Data Race ◽  
Sequential Program ◽  
Functional Correctness ◽  
Correct Program ◽  
Basic Blocks

AbstractA commonly used approach to develop deterministic parallel programs is to augment a sequential program with compiler directives that indicate which program blocks may potentially be executed in parallel. This paper develops a verification technique to reason about such compiler directives, in particular to show that they do not change the behaviour of the program. Moreover, the verification technique is tool-supported and can be combined with proving functional correctness of the program. To develop our verification technique, we propose a simple intermediate representation (syntax and semantics) that captures the main forms of deterministic parallel programs. This language distinguishes three kinds of basic blocks: parallel, vectorised and sequential blocks, which can be composed using three different composition operators: sequential, parallel and fusion composition. We show how a widely used subset of OpenMP can be encoded into this intermediate representation. Our verification technique builds on the notion of iteration contract to specify the behaviour of basic blocks; we show that if iteration contracts are manually specified for single blocks, then that is sufficient to automatically reason about data race freedom of the composed program. Moreover, we also show that it is sufficient to establish functional correctness on a linearised version of the original program to conclude functional correctness of the parallel program. Finally, we exemplify our approach on an example OpenMP program, and we discuss how tool support is provided.

Tool Support for Confidentiality-by-Construction

2019 ◽  
Vol 38 (2) ◽  
pp. 64-68
Author(s):  
Tobias Runge ◽  
Ina Schaefer ◽  
Alexander Knüppel ◽  
Loek Cleophas ◽  
Derrick Kourie ◽  
...  
Keyword(s):  
Tool Support

scholarly journals Security assurance cases—state of the art of an emerging approach

2021 ◽  
Vol 26 (4) ◽  
Author(s):  
Mazen Mohamad ◽  
Jan-Philipp Steghöfer ◽  
Riccardo Scandariato
Keyword(s):  
State Of The Art ◽  
Tool Support ◽  
Security Assurance ◽  
The Past ◽  
Depth Analysis ◽  
Structured Argumentation ◽  
Security Properties ◽  
Standards And Regulations ◽  
Assurance Cases ◽  
Security Standards

AbstractSecurity Assurance Cases (SAC) are a form of structured argumentation used to reason about the security properties of a system. After the successful adoption of assurance cases for safety, SAC are getting significant traction in recent years, especially in safety-critical industries (e.g., automotive), where there is an increasing pressure to be compliant with several security standards and regulations. Accordingly, research in the field of SAC has flourished in the past decade, with different approaches being investigated. In an effort to systematize this active field of research, we conducted a systematic literature review (SLR) of the existing academic studies on SAC. Our review resulted in an in-depth analysis and comparison of 51 papers. Our results indicate that, while there are numerous papers discussing the importance of SAC and their usage scenarios, the literature is still immature with respect to concrete support for practitioners on how to build and maintain a SAC. More importantly, even though some methodologies are available, their validation and tool support is still lacking.

Reconfigurable Instruction-Set Application-Tuning for DSP

2003 ◽  
Vol 12 (03) ◽  
pp. 333-351 ◽  
Author(s):  
B. Mesman ◽  
Q. Zhao ◽  
N. Busa ◽  
K. Leijten-Nowak
Keyword(s):  
Current System ◽  
High Volume ◽  
Tool Support ◽  
Instruction Set ◽  
Instruction Sets ◽  
Application Characteristics ◽  
On Chip ◽  
Application Tuning ◽  
Primary Contribution ◽  
Hardware Efficiency

In current System-on-Chip (SoC) design, the main engineering trade-off concerns hardware efficiency and design effort. Hardware efficiency traditionally regards cost versus performance (in high-volume electronics), but recently energy consumption emerged as a dominant criterion, even in products without batteries. "The" most effective way to increase HW efficiency is to exploit application characteristics in the HW. The traditional way of looking at HW design tends to consider it a time-consuming and tedious task, however. Given the current lack of HW designers, and the pressure of time-to-market, clearly a desire exists to fine-balance the merits and effort of tuning your HW to your application. This paper discusses methods and tool support for HW application-tuning at different levels of granularity. Furthermore we treat several ways of applying reconfigurable HW to allow both silicon reuse and the ability to tune the HW to the application after fabrication. Our main focus is on a methodology for application-tuning the architecture of DSP datapaths. Our primary contribution is on reusing and generalizing this methodology to application-tuning DSP instruction sets, and providing tool support for efficient compilation for these instruction sets. Furthermore, we propose an architecure for a reconfigurable instruction-decoder, enabling application-tuning of the instruction-set after fabrication.

scholarly journals Tool support for assurance case development

2017 ◽  
Vol 25 (3) ◽  
pp. 435-499 ◽  
Author(s):  
Ewen Denney ◽  
Ganesh Pai
Keyword(s):  
Tool Support ◽  
Case Development ◽  
Assurance Case
Sign in / Sign up

Export Citation Format

Share Document