ABSTRACT. A part of the reason of student’s and engineer’s poor attitude to Formal Methods, is very simple: FM-experts do not care about primary education in this field at the early stage of higher education. In particular, many courses on Formal Semantics start with fearful terms like state machine, logic inference, denotational semantics, etc., without elementary explanations of the basic notions.

ABSTRACT. Algebras describing higher order programming notions in a maximally abstract manner (general algebraic program structures, GAPS) are introduced and investigated. The criterion when given programming language can be enriched by a system of program transformations is stated and proved. Specializations of GAPS for fully invertible and injective programs are investigated. Numerous examples are presented.

ABSTRACT. Over the past year, we have been developing Chekofv, a system for crowd-sourced formal verification. Chekofv starts with an at- tempt to verify a given C program using the source code analysis plat- form Frama-C. Every time the analysis loses precision while analyzing looping control-flow, Chekofv tries to obtain an invariant to regain precision using crowd-sourcing. To that end, Chekofv translates the problem of finding loop invariants into a puzzle game and presents it to players of a game, Xylem, that is being developed as part of the Chekofv system. In this paper, we report on the design and implementation of the Chekofv system, the challenges and merits of gamification of the invariants detection problem, and problems and obstacles that we have encountered so far.

ABSTRACT. The talk presents an approach to undergraduate teaching of formal semantics of programs. It explains what is formal semantics by developing operational, denotational and axiomatic semantics for an ``esoteric'' language. We hope that the approach will be interesting to communities of Program Theoreticians and Software Engineers, that it will help better education to bridge a cultural gap between Formal Methods theories and Software Engineering practice.

ABSTRACT. “In the end, you are a mathematician, not a computer scientist” or “Have we not already discovered everything in computer science?”. Which theoretical computer scientist has not heard a similar sentence when trying to explain hir research to a layperson? Promotion of theoretical computer science, and formal methods in particular, is mainly hindered by the high level of abstraction commonly used in the field, and probably furthermore complicated by a lack of education of the people thereupon.

We present in this paper an educational experiment intended to explain the importance and aim of formal methods, along with the challenges they present. It uses Lego robots as an anchor to the real world, introducing fun into the presentation. Primarily targeting high-school students, it forms a solid and adaptable basis to reach various audiences.

ABSTRACT. Abstract. Courcelle's celebrated theorem forms a strong theoretical basis for the development of formal methods. This extended abstract argues that a good intuition into the underlying ideas behind Courcelle's theorem can be achieved by considering the applications of these ideas to combinatorics. Technical notions regarding compuation are eliminated and replaced with simple notions of recurrence relations.

ABSTRACT. Process engineering deals with the design, operation and optimization of different physical processes such as chemical reactions, biological mechanisms and petroleum processing. Recent technological advancements and short time to market in almost every industry bring new challenges and hence the complexity in the process engineering systems. One of the main techniques to analyze such models is to represent underlying systems using signal-flow-graphs which provide a systematic procedure to evaluate the system performance in the form of transfer functions. Traditionally, the analysis of signal-flow-graphs based models has been carried out by the paper-and-pencil based proofs and numerical techniques. In this paper, we present an overview of using theorem proving to formally analyze processing engineering models. The main motivation of this work is twofold: First, the application of formal methods in new domain to improve the analysis accuracy; Second, an effort to reduce the gap between formal methods and different engineering communities such as mechanical, chemical and engineering management.

ABSTRACT. Concurrency and synchronization is an important behavior of hardware and software systems. Finding defects in the late phase of system development process is not acceptable anymore in industrial applications because of its highly capital investment in modern complex systems. This paper demonstrates system verification by two approaches: model checking and proof checker. Here verification of a concurrent running architecture is demonstrated in both approaches to exhibit the requirement of fully formal verification method in order to generate a better hardware and software quality. To support this, we will describe how the proof checker is used for complete verification of a system in terms of any input size and complexity.