Dov M. Gabbay

Reiner Hähnle

M. D'Agostino

J. Posegga

Recent years have been blessed with an abundance of logical systems, arising from a multitude of applications. A logic can be characterised in many different ways. Traditionally, a logic is presented via the following three components: 1. an intuitive non-formal motivation, perhaps tie it in to some application area 2. a semantical interpretation 3. a proof theoretical formulation. There are several types of proof theoretical methodologies, Hilbert style, Gentzen style, goal directed style, labelled deductive system style, and so on. The tableau methodology, invented in the 1950s by Beth and Hintikka and later per fected by Smullyan and Fitting, is today one of the most popular, since it appears to bring together the proof-theoretical and the semantical approaches to the pre of a logical system and is also very intuitive. In many universities it is sentation the style first taught to students. Recently interest in tableaux has become more widespread and a community crystallised around the subject. An annual tableaux conference is being held and proceedings are published. The present volume is a Handbook a/Tableaux pre senting to the community a wide coverage of tableaux systems for a variety of logics. It is written by active members of the community and brings the reader up to frontline research. It will be of interest to any formal logician from any area.

Handbook of Tableau Methods

Frank S. de Boer

Marcello M. Bonsangue

Elena Giachino

This book constitutes revised lectures from the 11th Symposium on Formal Methods for Components and Object, FMCO 2012, held in Bertinoro, Italy, in September 2012. The 8 lectures featured in this volume are by world-renowned experts within the area of formal models for objects and components. The book provides a unique combination of ideas on software engineering and formal methods which reflect the expanding body of knowledge on modern software systems.

11th International Symposium, FMCO 2012, Bertinoro, Italy, September 24-28, 2012, Revised Lectures

Formal Methods for Components and Objects

Peter H. Schmitt

Bernhard Beckert

The ultimate goal of program verification is not the theory behind the tools or the tools themselves, but the application of the theory and tools in the software engineering process. Our society relies on the correctness of a vast and growing amount of software. Improving the software engineering process is an important, long-term goal with many steps. Two of those steps are the KeY tool and this KeY book.

Foreword by K. Rustan M. Leino

Verification of Object-Oriented Software. The KeY Approach

Jürgen Giesl

This volume contains the proceedings of the 5th International Joint Conference on Automated Reasoning (IJCAR 2010). IJCAR 2010 was held during July 16-19 as part of the 2010 Federated Logic Conference, hosted by the School of Informatics at the University ofEdinburgh,Scotland. Support by the conference sponsors – EPSRC, NSF, Microsoft Research, Association for Symbolic Logic, CADE Inc. , Google, Hewlett-Packard, Intel – is gratefully acknowledged. IJCARisthepremierinternationaljointconferenceonalltopicsinautomated reasoning, including foundations, implementations, and applications. Previous IJCAR conferences were held at Siena (Italy) in 2001, Cork (Ireland) in 2004, Seattle (USA) in 2006, and Sydney (Australia) in 2008. IJCAR comprises s- eral leading conferences and workshops. In 2010, IJCAR was the fusion of the following events: –CADE: International Conference on Automated Deduction –FroCoS: International Symposium on Frontiers of Combining Systems –FTP: International Workshop on First-Order Theorem Proving – TABLEAUX: InternationalConferenceonAutomatedReasoningwith- alytic Tableaux and Related Methods There were 89 submissions (63 regular papers and 26 system descriptions) of which 40 were accepted (28 regular papers and 12 system descriptions). Each submission was assigned to at least three Program Committee members, who carefully reviewed the papers, with the help of 92 external referees. Afterwards, the submissions were discussed by the ProgramCommittee during two weeks by means of Andrei Voronkov’s EasyChair system. We want to thank Andrei very much for providing his system, which was very helpful for the management of the submissions and reviews and for the discussion of the Program Committee.

5th International Joint Conference, IJCAR 2010, Edinburgh, UK, July 16-19, 2010, Proceedings

Automated Reasoning

Amel Bennaceur

Karl Meinke

Machine learning of software artefacts is an emerging area of interaction between the machine learning and software analysis communities. Increased productivity in software engineering relies on the creation of new adaptive, scalable tools that can analyse large and continuously changing software systems. These require new software analysis techniques based on machine learning, such as learning-based software testing, invariant generation or code synthesis. Machine learning is a powerful paradigm that provides novel approaches to automating the generation of models and other essential software artifacts. This volume originates from a Dagstuhl Seminar entitled "Machine Learning for Dynamic Software Analysis: Potentials and Limits” held in April 2016. The seminar focused on fostering a spirit of collaboration in order to share insights and to expand and strengthen the cross-fertilisation between the machine learning and software analysis communities. The book provides an overview of the machine learning techniques that can be used for software analysis and presents example applications of their use. Besides an introductory chapter, the book is structured into three parts: testing and learning, extension of automata learning, and integrative approaches.

International Dagstuhl Seminar 16172, Dagstuhl Castle, Germany, April 24-27, 2016, Revised Papers

Machine Learning for Dynamic Software Analysis: Potentials and Limits

This volume contains the research papers, invited papers, and abstracts of - torials presented at the Second International Conference on Tests and Proofs (TAP 2008) held April 9–11, 2008 in Prato, Italy. TAP was the second conference devoted to the convergence of proofs and tests. It combines ideas from both areasfor the advancement of softwarequality. To provethe correctnessof a programis to demonstrate, through impeccable mathematical techniques, that it has no bugs; to test a programis to run it with the expectation of discovering bugs. On the surface, the two techniques seem contradictory: if you have proved your program, it is fruitless to comb it for bugs; and if you are testing it, that is surely a sign that you have given up on anyhope of proving its correctness.Accordingly,proofs and tests have,since the onset of software engineering research, been pursued by distinct communities using rather di?erent techniques and tools. And yet the development of both approaches leads to the discovery of c- mon issues and to the realization that each may need the other. The emergence of model checking has been one of the ?rst signs that contradiction may yield to complementarity, but in the past few years an increasing number of research e?orts have encountered the need for combining proofs and tests, dropping e- lier dogmatic views of their incompatibility and taking instead the best of what each of these software engineering domains has to o?er.

Second International Conference, TAP 2008, Prato, Italy, April 9-11, 2008, Proceedings

Tests and Proofs

Wil van der Aalst

This book is Open Access under a CC BY licence. This book constitutes the proceedings of the 22nd International Conference on Fundamental Approaches to Software Engineering, FASE 2019, which took place in Prague, Czech Republic in April 2019, held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019.The 24 papers presented in this volume were carefully reviewed and selected from 94 submissions. The papers are organized in topical sections named: software verification; model-driven development and model transformation; software evolution and requirements engineering; specification, design, and implementation of particular classes of systems; and software testing.

22nd International Conference, FASE 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings

Fundamental Approaches to Software Engineering

Richard Bubel

Wolfgang Ahrendt

Mattias Ulbrich

Static analysis of software with deductive methods is a highly dynamic field of research on the verge of becoming a mainstream technology in software engineering. It consists of a large portfolio of - mostly fully automated - analyses: formal verification, test generation, security analysis, visualization, and debugging. All of them are realized in the state-of-art deductive verification framework KeY. This book is the definitive guide to KeY that lets you explore the full potential of deductive software verification in practice. It contains the complete theory behind KeY for active researchers who want to understand it in depth or use it in their own work. But the book also features fully self-contained chapters on the Java Modeling Language and on Using KeY that require nothing else than familiarity with Java. All other chapters are accessible for graduate students (M.Sc. level and beyond).“/p> “/p> The KeY framework is free and open software, downloadable from the book companion website which contains also all code examples mentioned in this book.

Reiner Hähnle

Books

Your next favorite book is out there