Extensive research on formal verification of machine learning systems indicates that learning from data alone often fails to capture underlying background knowledge, such as specifications implicitly available in the data. Various neural network verifiers have been developed to ensure that a machine-learnt model satisfies correctness and safety properties; however, they typically assume a trained network with fixed weights. A promising approach for creating machine learning models that inherently satisfy constraints after training is to encode background knowledge as explicit logical constraints that guide the learning process via so-called differentiable logics. In this paper, we experimentally compare and evaluate various logics from the literature, present our findings, and highlight open problems for future work. We evaluate differentiable logics with respect to their suitability in training, and use a neural network verifier to check their ability to establish formal guarantees. The complete source code for our experiments is available as an easy-to-use framework for training with differentiable logics at https://github.com/tflinkow/comparing-differentiable-logics .

Python is a highly popular programming language, used across a broad range of domains from web servers to autonomous robots. Thus, to ensure correctness of these software systems, it is essential to develop good software verification tooling that is useable and well-integrated with Python. To this end we propose a model checker designed specifically for Python that would identify potential errors, and ease the development and testing process. We discuss what would be desirable in such a model checker and present our work in progress, with an approach inspired by Java Pathfinder, along with plans for future development.

The theory of institutions provides an abstract mathematical framework for specifying logical systems and their semantic relationships. Institutions are based on category theory and have deep roots in a well-developed branch of algebraic specification. However, there are no machine-assisted proofs of correctness for institution-theoretic constructions—chiefly satisfaction conditions for institutions and their (co)morphisms—making them difficult to incorporate into mainstream formal methods. This paper therefore provides the details of our approach to formalizing a fragment of the theory of institutions in the Coq proof assistant. We instantiate this framework with the institutions FOPEQ for first-order predicate logic and EVT for the Event-B specification language, and define some institution-independent constructions, all of which serve as an illustration and evaluation of the overall approach.

This paper describes an unplugged computational thinking (CT) resource for primary and secondary schools developed from Bebras tasks. In Ireland, CT is not part of the primary school curriculum or mandatory in secondary schools. However, the National Council for Curriculum and Assessment is in the process of revising the primary school curriculum to include aspects of CT. Our aim for creating this CT Obstacle Course is to introduce teachers (and pupils) without formal computer science training to the subject of CT. This is done in a manner that informs and motivates, and gives them the confidence to deliver CT materials in the classroom. We also want to find out from teachers how useful and important this type of resource is for developing problem-solving skills, and if our unplugged activity can support learning at various skill levels. Our CT Obstacle Course includes 14 Bebras tasks for primary schools and an additional 6 Bebras tasks for secondary schools. The activity is suitable for indoors and outdoors and is completed in groups, promoting teamwork and communication. We have delivered it to 146 primary school classes during 38 school visits between May 2021 and June 2022. It has been undertaken by 3,445 pupils and 195 teachers and other school staff. This paper describes our CT resource in detail, and reports teacher feedback from primary schools.

In this poster, we highlight computational thinking resources for schools from the PACT team at Maynooth University, Ireland. The resources are derived from tasks from the Bebras international computational thinking initiative. The different modalities work together throughout the school year to provide initial exposure to computational thinking, and include an obstacle course, seasonal tasks, and a workbook.

This special collection arose from the 17th International Conference on integrated Formal Methods (iFM) held in beautiful Lugano, Switzerland, hosted by the Software Institute of USI Università della Svizzera italiana.

This paper describes our process of creating computational thinking (CT) resources for primary school teachers in Ireland. The National Council for Curriculum and Assessment has proposed a revised primary mathematics curriculum with an emphasis on CT skills and problem solving, and some teachers would like to introduce it already on an informal basis. However, CT is not yet part of teacher training. Our motivating question has been: how can teachers without a computer science background deliver CT at primary level in Ireland? Our process involves third-level computer science academics co-creating resources with in-service and pre-service teachers during workshops. The resources comprise a workbook and lesson plans. Our resources are based on tasks from the International Bebras Challenge, a well-known large-scale international CT contest with a reasonably gender-neutral profile of school-age participants. The workbook consists of ten Bebras tasks, each followed by a page of original activities on the theme of the task. A set of ten lesson plans accompanies the workbook. Each lesson plan has information about how to use the corresponding workbook activities in the classroom, where the activity might fit into the existing curriculum, categorisation of the task in terms of eight CT topics, differentiation, and extension activities. This paper explains our process of workshop planning, workbook creation, and lesson plan co-creation. Preliminary evaluation of our process uses teacher feedback.

This paper describes a formal semantics for the Event-B specification language using the theory of institutions. We define an institution for Event-B, EVT, and prove that it meets the validity requirements for satisfaction preservation and model amalgamation. We also present a series of functions that show how the constructs of the Event-B specification language can be mapped into our institution. Our semantics sheds new light on the structure of the Event-B language, allowing us to clearly delineate three constituent sub-languages: the superstructure, infrastructure and mathematical languages. One of the principal goals of our semantics is to provide access to the generic modularisation constructs available in institutions, including specification-building operators for parameterisation and refinement. We demonstrate how these features subsume and enhance the corresponding features already present in Event-B through a detailed study of their use in a worked example. We have implemented our approach via a parser and translator for Event-B specifications, EBtoEVT, which also provides a gateway to the Hets toolkit for heterogeneous specification.

This paper provides an experience report of using the Dafny program verifier, at the VerifyThis 2021 program verification competition. The competition aims to evaluate the usability of logic-based program verification tools in a controlled experiment, challenging both the verification tools and the users of those tools. We present the two challenges that we tackled during the competition and discuss our solutions. As a result, we identify strengths and weaknesses of Dafny in the verification of relatively complex algorithms, and report on our experience of applying Dafny in this setting.

Abstract VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties—something that lies beyond the capabilities of fully automatic verification and requires instead human expertise to suitably encode programs, specifications, and invariants. This paper describes the 8th edition of VerifyThis, which took place at ETAPS 2019 in Prague. Thirteen teams entered the competition, which consisted of three verification challenges and spanned 2 days of work. This report analyzes how the participating teams fared on these challenges, reflects on what makes a verification challenge more or less suitable for the typical VerifyThis participants, and outlines the difficulties of comparing the work of teams using wildly different verification approaches in a competition focused on the human aspect.

This is an excellent book, which I am delighted to have the chance to review.I have used the first edition of this book to introduce decision procedures to graduate and undergraduate students studying software verification techniques.The text and the supporting material have been invaluable, stepping the reader through decision procedures and their combinations.The second edition offers both an updated introduction to the topic of decision procedures and more advanced material concerning topics such as quantification, efficiency in SAT solving and applications of SMT solving in industry.The authors focus on decision procedures for decidable first-order theories that are used primarily in automated software and hardware verification as well as theorem proving.Decision procedures are presented with clear definitions, algorithms and updated examples representative of real-world problems.It is suitable for advanced undergraduate students, MSc level graduates and research students.I have read the book in detail and compared it to the first edition.Chapters 1, 2 and 3 provide an overview of basic concepts and material required to understand satisfiability.In this second edition, the focus has moved from the DPLL framework to Conflict-Driven Clause Learning (CDCP) based procedures for deciding propositional formulae and more detail is provided on SAT solvers and the constraint satisfaction problem (SCP).This is a sensible update as it coincides with advances in tools for SAT and SMT solving.Chapter 3 provides an extended coverage of DPLL(T), a generalisation of CDCL to a decision procedure for decidable quantifier-free first-order theories.This is updated and made central to the text from the first edition, where DPLL(T) was discussed in a subsection of Chapter 11.This update is welcome as DPLL(T) is implemented in many current SMT solvers.As before chapter 4-10 are self contained, covering equality logic, uninterpreted functions, linear arithmetic, bit vectors, arrays, pointer logic, quantified formulae and the decidability of their combinations via the Nelson-Oppen Combination Procedure.Chapter 11 discusses lazy and eager encodings, focusing on eager approaches for eliminating uninterpreted functions via a reduction to equality logic constraints.Graph based methods for an eager encoding of equality logic formulae into propositional logic are also described.This chapter reorganises material from the first edition of the book, bringing it together to discuss the topic as an alternative to the DPLL(T) approach.Chapter 12 offers new material which describes industrial applications in Software Engineering and Computational Biology, with sections contributed from researchers at Microsoft Research.Topics presented, and supporting examples, are interesting for both researchers and students learning about SAT and SMT, covering topics such as bounded and unbounded program analysis, DNA computing and gene regulatory networks.A short SMT-Lib tutorial (in the appendices) is a further welcome addition to the text.

VerifyThis 2015 was a one-day program verification competition which took place on April 12th, 2015 in London, UK, as part of the European Joint Conferences on Theory and Practice of Software (ETAPS 2015). It was the fourth instalment in the VerifyThis competition series. This article provides an overview of the VerifyThis 2015 event, the challenges that were posed during the competition, and a high-level overview of the solutions to these challenges. It concludes with the results of the competition and some ideas and thoughts for future instalments of VerifyThis.

In this paper we present an approach to generating instances of metamodels using a Satisfiability Modulo Theories (SMT) solver as a back-end engine. Our goal is to automatically translate a metamodel and its invariants into SMT formulas which can be investigated for satisfiability by an external SMT solver, with each satisfying assignment for SMT formulas interpreted as an instance of the original metamodel. Our automated translation works by interpreting a metamodel as a bounded Attributed Type Graph with Inheritance (ATGI) and then deriving a finite universe of all bounded attribute graphs typed over this bounded ATGI. The graph acts as an intermediate representation which we then translate into SMT formulas. The full translation process, from metamodels to SMT formulas, and then from SMT instances back to metamodel instances, has been successfully automated in our tool, with the results showing the feasibility of this approach.

Perfect Developer is a software tool that supports the formal development of object-oriented programs by refinement, including formal verification of code. It is built around a single language that supports both specification and implementation. We critically examine how Perfect Developer supports programming by refinement, focusing on three refinement techniques: algorithm refinement, data refinement and delta refinement. In particular we examine the extent to which Perfect Developer provides formal verification for these techniques. We assess it as a tool for software construction and compare it with related tools.