Volume •Abstracts •Preface •Authors •Keywords •BibTex Entries

ATx'12/WInG'12: Volume Information

ATx'12/WInG'12: Joint Proceedings of the Workshops on Automated Theory eXploration and on Invariant Generation

Editors: Jacques Fleuriot, Peter Höfner, Annabelle McIver and Alan Smaill

EPiC Series in Computing•Volume 17

7 articles•70 pages•Published: July 28, 2013

Papers

Proof Assistants and the Dynamic Nature of Formal Theories

Robert L. Constable

1-15

HipSpec : Automating Inductive Proofs of Program Properties

Koen Claessen, Moa Johansson, Dan Rosen and Nick Smallbone

16-25

Synthesising Graphical Theories

Aleks Kissinger

26-35

A Framework for Verified Depth-First Algorithms

36-45

Theory Exploration: a role for Model Theory?

46-53

Specification Inference and Invariant Generation: A Machine Learning Perspective

54

Abstract Domains for Bit-Level Machine Integer and Floating-point Operations

55-70

Keyphrases

abstract interpretation, automated induction, automated theorem proving, categorical quantum mechanics, Conjecture synthesis, depth-first search, equational reasoning, floating-point numbers, graph rewriting, Isabelle/HOL, machine integers, model checking, model theory, monoidal categories, numeric domains, program verification, saturation, static analysis, string diagrams, testing, theorem proving, theory exploration, theory formation.