In this column, algebra again takes center stage. Here I offer substantial challenges for you.
I was first introduced to the notion of proof when I entered the math
department at the University of Chicago as a graduate student.
I was treated to lectures by I. J. Kaplansky, Paul Halmos, and others who
proved one theorem after another.
For example, suppose that the theorem was to prove commutativity for groups in
which the square of x, for all x, is the identity
e.
Then, if a proof was offered, on the blackboard
would appear a series of equations the last of which would be xy = yx.
For that problem, the assumption that commutativity was not present was not
used (as the proof proceeded), namely, the assumption that ab ≠ ba for constants a and b.
In particular, I did not often witness a proof by contradiction.
Instead, typically all the steps of the proof were obtained by forward reasoning,
reasoning from axioms and other properties.
Such a proof is called a direct proof.
If, at the time (in the early 1950s), the intention was to automate the finding of proofs, the
programmer (if such existed), seeking a direct proof, could have placed, say,
xy = yx on some list and continually
compared the conclusions drawn by the program to see whether the goal had
been reached.
From the viewpoint of history, computer programs were not around in the early 1950s in general -- none, certainly, for automated reasoning.
In contrast, if this theorem were given to an automated reasoning program of
the type I rely on today, then as part of the input I would include a clause
asserting ab ≠ ba for constants a and b.
The program, if successful, would return a proof by contradiction, using the
given inequality.
Now, if this inequality were used to detect unit conflict and in no other way, then all the reasoning offered by the program would be forward reasoning. Such a proof is called a forward proof. On the other hand, if the program offered a proof none of whose steps relied purely on axioms and various hypotheses, then the proof is a backward proof. And if the proof exhibited both forward and backward reasoning, it is a bidirectional proof. Bidirectional proofs are frequently easier to obtain with an automated reasoning program. One reason rests with the level of a bidirectional proof. You might say that compared with either a forward or backward proof, a bidirectional proof (so to speak) meets in the middle. (If the only inference rule in use is condensed detachment, however, then for efficiency forward reasoning had best be used.)
The proofs under discussion here are first-order proofs, in contrast to higher-order proofs that some reasoning programs can find, as with M. Beeson's extension of OTTER.
All proofs yielded by OTTER, Bill McCune's splendid contribution to the
field, focus on first-order reasoning.
My particular preference is for forward proofs (as opposed to bidirectional proofs), if such can be found with the
program in use and within the constraints imposed.
For the given example, I would ideally prefer a proof that completes with
xy = yx.
But for reasons regarding instantiation and the lack of appropriate strategy to control its use,
the proofs I have found, in my research, are proofs by contradiction.
In particular, for example, I never find a proof that deduces xy = yx, which is the desired conclusion to be proved for groups of exponent 2.
Proofs by contradiction are what are usually sought in automated reasoning, in contrast to proofs that simply terminate with the discovery of the sought-after goal;
the discovery of a contradiction provides an excellent (so-to-speak) stop
condition.
I now turn to the set of challenges and, specifically, to an achievement made by Bob Veroff in 2005. The theorem that was offered is taken from median algebra. A proof of the theorem did exist, but no first-order proof existed, from what I know, until Veroff found one. The following axioms for median algebra are to be used.
% Following 4 axioms for median algebra, from Veroff in turn from D. Knuth. f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). f(f(x,w,y),w,z) = f(x,w,f(y,w,z)) # label(associativity).(Yes, the problem was conveyed by Knuth to Veroff.)
For the target, the conclusion of the theorem, I present it in two forms, each negated, by interchanging the arguments.
% Denial of distributivity, as recently sent by Veroff. f(f(a1,a2,a3),a4,a5) != f(f(a1,a4,a5),f(a2,a4,a5),f(a3,a4,a5)) | $ANS(DIST). % Alternative denial of distributivity, as recently sent by Veroff. f(f(a1,a4,a5),f(a2,a4,a5),f(a3,a4,a5)) != f(f(a1,a2,a3),a4,a5) | $ANS(DIST).For the first challenge, you are asked to obtain a proof of any type, but the proof must be first-order. For your second challenge, you are asked to find a proof in which no demodulation occurs. (As many of you know, I prefer proofs in which demodulation is not relied upon.) In other words, you are asked to find a proof without relying on a Knuth-Bendix approach. For your third challenge, you are asked to find a proof that is forward, using denial only at the so-called unit conflict stage. A proof that uses a denial, such as
ab ≠ ba, only for unit conflict but not for drawing conclusions is, of course, a forward proof.
One more challenge might indeed prove intriguing and perhaps be most difficult to meet. The challenge is in the context of proof elegance, a topic I addressed in the book titled Automated Reasoning and the Discovery of Missing and Elegant Proofs. Specifically, you are asked to find a proof of distributivity from the given axioms, a proof that is free of demodulation, that is based on forward reasoning, and -- the aspect of elegance -- that has a length less than or equal to 50 (as measured in the number of deduced equations).
I plan in a future column to focus on an aspect of elegance different from that of concern in this last challenge.
The main goal of the ARCADE workshop was to bring together key people from various sub-communities of automated reasoning to discuss the present, past, and future of the field. ARCADE invited non-technical position statements of 2-4 pages. Out of 19 submitted abstracts the program committee selected 14 for presentation and discussion at the workshop.
With its 45 attendees, the first installment of the ARCADE workshop was half as large as CADE itself. Several participants came to Gothenburg only or mainly because of ARCADE.
The workshop was divided into five sessions. Each session consisted of 2-3 short talks of either 5 or 10 minutes followed by a discussion of the presented topics driven by questions submitted by the authors. The accepted abstracts and proposed questions were published on the workshop's web-page in advance of the workshop to allow attendees to consider these points beforehand. In the following we present an incomplete but representative selection of highlights from the discussion sessions.
The first session discussed how to bridge the gaps between the various sub-communities of automated reasoning (AR) as well as the even wider gaps between automated reasoning and other communities. James Davenport highlighted some of the very basic problems, including varying terminology across communities, which popped up in the SC2 project about combining SMT solvers and computer algebra systems. To make progress for SC2, patience and many dialogues were necessary. A discussion around combining AR methods concluded that simple and elegant tools with good interfaces are a prerequisite to success.
The topic of the second session was machine learning (ML) and more generally artificial intelligence (AI). Although historically AR was a part of AI, Maria Paola Bonacina made the point that AI has become synonymous with ML, while AR has become a second choice technology in cases where ML fails. As a community we cannot be satisfied with this status, but the immediate countermeasures remain unclear. Various ways of combining AR and ML have been discussed: namely, to use AR to explain the decision made by ML and to use ML to guide the search in AR. The idea of a joint workshop bringing AR and ML together was proposed.
The next session dealt with the user friendliness of AR tools and their
applicability in industry. Marijn Heule presented the industry success story of
the ACL2 proof assistant. The key to success was that success in industry
was
an original design goal of ACL2. Yet, the needs of industry were not
necessarily aligned with the research directions in AR. Industry cares about
usability and efficiency, but not so much about completeness. A suggestion was
made that we become more user-driven, with support (through calls for papers
etc.) for experimental user studies, and support for industry-focused problems
in competitions. Reiner Hähnle pointed out that to sustainably support this
through funding agencies, computer science in general needs to be reclassified
as an engineering science (as opposed to a theoretical science).
The fourth session focused on methods to make proofs produced by systems more
easily checkable. For proofs produced by SAT solvers this meant including
reasoning about absence of formulas (e.g., clause deletion in DRAT) and
advanced features used by SAT solvers (e.g., symmetry breaking) in the proof
format. In the case of first-order (FO) solvers the solution is less clear and
the consensus was that it is hard to go beyond the very general standardized
semantic-less TSTP proof format, as there is no agreement on the prime
FO
calculus.
The last session dealt with current challenges for actual reasoners, such as
lifting answer set programs to first-order, adding synthesis to SMT via
quantifier instantiation, and extracting common principles (Model Portfolio
)
from different calculi for fragments of first-order logic. In the discussion,
it was observed that the common principle of those challenges was the
identification of a weak spot in existing approaches. A resulting consideration
was to focus the evaluation of reasoners around the number of uniquely solved
problems. Geoff Sutcliffe confirmed that the CASC competition measures this,
but does not reward tools that perform well according to this metric.
In a final round of discussion, we considered various constellations of N
authors and M pages for a document that would summarize the state-of-the-art in
AR and upcoming challenges. For N > 40 and M < 5, an idea of a CACM article on
the challenges in AR was discussed. Another proposal was a survey of AR, with
N < 20 and M > 40. For N = 1 and M > 300, an more up-to-date textbook than the
Handbook of Automated Reasoning
to attract new PhD students was considered
helpful. In this space, John Harrison's Handbook of Practical Logic and
Automated Reasoning
is a good hands-on introduction to many topics, but it is
deliberately selective in what it covers to keep things elementary
. Rumors tell
that Christoph Weidenbach is working on another textbook draft.
After the workshop, the authors have been invited to update their original submissions with respect to the discussions held and to submit them to a post-proceedings that will be published as an EPiC volume. Additionally, attendees have been invited to submit papers covering points that arose from the discussions. The aim is for the post-proceedings to appear in October.
The organization of ARCADE was very smooth and easy going, mainly due to the great support that we received from the CADE community. We thank Christoph Weidenbach, who initiated the workshop and jointly with Jasmin Blanchette helped recruiting most of the program committee. We are very grateful to Wolfgang Ahrendt and the local organization team for taking great care of everything on-site and reserving the venue for the ARCADE dinner. The latter was suggested by Reiner Hähnle and turned out to be a great choice. We thank the program committee (and one sub-reviewer) for detailed, careful, and constructive reviews and the pleasant discussion. This report benefited from notes taken by James Davenport during the workshop and from Jasmin Blanchette's comments. Finally, we thank the authors and the attendees for creating such a diverse and timely program and discussion that will certainly have an impact on the future of automated reasoning.
In the guest column of AAR Newsletter No. 120 (June 2017) Christoph Weidenbach proposes as challenge the development of automated reasoning procedures that search simultaneously for a proof or a counter-model. While the idea itself is not new, since for example Ricardo Caferra and Nicolas Zabel had an article entitled A method for simultaneous search for refutations and models by equational constraint solving as early as 1992, I agree that the time is ripe given the awsome advances of our field as witnessed this summer at CADE-26 and Big Proof. Model-based methods appear a natural starting point for this quest.
The purpose of this letter is to complement Chris' column
on the historical record of the first big proof that Chris mentions,
namely Bill McCune's
automated proof that Robbins algebra are Boolean,
of which Chris writes
The formalization of the Robbins conjecture is a problem in first-order
logic with equality. Bill designed a specific version of Otter, called EQP,
to fit exactly this problem.
First, the formalization of the Robbins theorem only requires equational logic.
Second,
EQP is not a version of
Otter:
it is a distinct theorem prover for reasoning in equational theories,
possibly with AC operators,
while Otter is a theorem prover for full first-order logic with equality.
Third,
saying that EQP was designed "to fit exactly" the Robbins problem
is too strong and may be misunderstood as implying that EQP was
somehow ad hoc, which is not the case:
EQP is a generic prover for (AC) equational reasoning
in the same category as
Waldmeister.
In those years I was working on parallel theorem proving by Clause-Diffusion, using Bill's code as sequential base for the Clause-Diffusion provers. I visited Argonne, and Bill and I were in correspondence by e-mail for years. Bill told me that he wrote EQP because he felt that Otter had become big, with many options and parameters, and Bill wanted a leaner prover to experiment with. In hindsight, clearly the Robbins conjecture was one of the objectives of this experimentation, but there is no historical evidence that I know of to suggest that it was the only one: Bill was interested in automated reasoning in mathematics and specifically in algebraic structures presented by sets of equations, often including associative and commutative (AC) operators. This goal requires high-performance equational reasoning and reasoning modulo AC. Bill decided that it was not a good idea to encapsulate these features in Otter as a special configuration and opted for developing a different prover.
For an idea of the differences between EQP and Otter, it suffices to consider that EQP features a main control loop, called the pair algorithm, that Otter does not have and that is different from Otter's given-clause algorithm. The concept of ordering-based strategies is to keep things small with respect to well-founded orderings. Thus, it is crucial to perform contraction (e.g., simplification, subsumption) with higher priority than expansion (e.g., ordered resolution, superposition, ordered paramodulation). In the given-clause loop at every iteration the prover selects a given clause and performs all expansion inferences between the given clause and all previously selected clauses. Then, it applies the newly generated clauses to reduce the previously existing ones, a process called backward contraction. If paramodulation is done modulo AC, there are many AC-paramodulants. Bill observed that generating all the AC-paramodulants between the given equation and all other previously selected equations before allowing backward contraction was detrimental for performance, because it meant too much expansion without contraction. Thus, he devised the pair algorithm, where at every iteration the prover selects a pair of equations and performs only the expansion inferences between them. The pair algorithm was a main ingredient in both sequential and parallel proofs of the Robbins theorem by EQP and its Clause-Diffusion parallelization Peers-mcd, respectively. This difference in the main control loop exemplifies how EQP and Otter are different provers.
We invite proposals for sites around the world to host the international Conference on Automated Deduction (CADE) to be held in summer 2019. CADE typically merges into IJCAR (the International Joint Conference in Automated Reasoning) in even years, and meets as an independent conference in odd years. For odd years, both proposals to host CADE alone or CADE co-located with other conferences are welcome. CADE's/IJCAR's recent location history is as follows:
The upcoming CADE/IJCAR event will be:
The deadline for proposals is 30 October 2017.
In addition, we encourage proposers to register their intention informally as soon as possible. The final selection of the site will be made within two months after the proposal due date.
Proposals should address the following points that also represent criteria for evaluation:
Prospective organizers are encouraged to get in touch with the CADE secretary and president (at martingi (at) ifi.uio.no and weidenbach (at) mpi-inf.mpg.de) for informal discussion. If the host institution is not actually located at the proposed site, then one or more visits to the site by the proposers is encouraged.
Martin Giese, Secretary of AAR and CADE
An election of CADE trustees will be held soon and all AAR members will receive a ballot. The following people (listed in alphabetical order) are currently serving as trustees of CADE Inc.:
The terms of Pascal Fontaine, Jürgen Giesl, and Geoff Sutcliffe end. There are thus three positions of elected trustees to fill.
The following candidates were nominated and there statements are below:
CADE was the first conference I attended as a PhD student and is my favorite conference to attend. I have always found the CADE community to be great at stimulating collaboration and new ideas among a range of researchers within automated deduction. I have attended every CADE and IJCAR since 2012 (as well as in 2009 and 2010), have sub-reviewed numerous papers, and had the pleasure serve on the program committee and as the co-organizer of workshops and competitions for CADE 25 in Berlin.
My research has focused on developing techniques in Satisfiability Modulo Theories (SMT) solvers. I am one of the main developers of the SMT solver CVC4, which is a frequent participant in the CASC competition. While most of the SMT community focuses on quantifier-free reasoning, my research has focused on new approaches that combine background theories and quantified formulas, and hence often aligns closely with the research at CADE. In the coming years, more tools within the automated theorem proving community will benefit from SMT solver back ends, and conversely SMT solvers will learn from techniques that target other logics.
As a member of the steering committee, I would further emphasize putting foundational research into practice. I believe that the many great ideas that come out of the CADE community should be applied more actively in academia and industry. I believe that competitions like CASC and SMT-COMP are a great driving force in encouraging researchers to develop tools that are efficient, robust and trustworthy. Another initiative that other conferences have added recently is an optional artifact submission associated with each accepted paper. I have participated in artifact evaluation committees for the CAV and POPL conferences and found them encourage higher quality and robust tools. An artifact evaluation submission is something for CADE to consider in the future.
I believe the CADE community should actively seek cross-fertilization with related fields like software verification and automated synthesis. Automated theorem provers already can play a more active role in these areas. For instance, constrained Horn clause solving and syntax-guided synthesis are two application-inspired disciplines that are converging with techniques for automated theorem proving. CADE is potentially a great place to bring these communities together. In particular, I believe it is important to encourage a broad range of workshops at CADE, as this is great way to encourage researchers from neighboring fields to attend CADE.
I participated in CADE/IJCAR for the first time in 2010, within FLoC in Edinburgh. Since then, CADE has been one of my favorite conferences because it balances theory, implementation and applications.
This is a balance that I have tried to pursue in my own research as well. My recent achievements include: the Conflict Resolution calculus, which is a lifting of the proof-theoretical aspects of CDCL to first-order logic, implemented in the Scavenger theorem prover; algorithms for compressing propositional and first-order resolution proofs generated by sat-solvers, SMT-solvers and ATPs, implemented in Skeptik; formalization of ontological arguments by Gödel, Leibniz and others in Coq and Isabelle.
I have served the CADE community by: chairing the PxTP and the UITP workshops; organizing the APPA (All about Proofs, Proofs for All) tutorials at the Vienna Summer of Logic; and creating and maintaining the Encyclopaedia of Proof Systems.
Looking forward, one of CADE's main challenges is to deal with the fact that automated deduction is a mature field, where a lot of great work has already been done; the entrance barrier is high, and the rewards for overcoming it are low. As a consequence, participation and submission numbers seem to be struggling to remain stable, and are low compared to conferences in other more popular computer science fields. This situation is problematic, especially for early-career researchers.
There are also challenges faced by the academic world as a whole (e.g. transparency, reproducibility of results, objectivity, diversity and inclusion, relevance to society...), and I believe CADE is in a good position to take a leading role in tackling these challenges among computer science conferences.
I have thought of a few concrete ideas to address these challenges. As an elected trustee, I would pursue only those ideas approved by a majority in this survey.
You can learn more about me in my website.As a trustee, my goal would be to keep the scope of CADE as broad as possible. CADE should be open to any aspect of automated deduction and it should cover everything from theoretical results and practical contributions up to applications of automated reasoning. It is important to make clear that every sub-field of automated reasoning is highly welcome at CADE to ensure CADE's position as the leading main conference of the field.
I also think that it is very important to attract tool submissions, and to organize tool competitions co-located with CADE. (Since its foundation in 2004, I have been active in the termination competition, which took place during IJCAR/CADE several times.)
I think the current organization of CADE as a stand-alone event every second year, within IJCAR every other year, and within FLoC every four years is a very good solution to guarantee the visibility of CADE on its own, while keeping in close contact with neighboring meetings and fields.
To attract as many participants as possible and to allow students to attend the conference, I think CADE should aim at affordable conference fees and continue the very good tradition of Woody Bledsoe travel grants for students.
My own research is concerned with different aspects of automated deduction. Therefore, I have been attending and publishing papers at CADE since 1994. In particular, I am working on techniques and tools to analyze properties like termination or complexity of programs automatically.
I was one of the PC chairs of IJCAR 2010, PC chair of RTA 2005, steering committee chair of RTA (2005-2007), area editor of ACM TOCL (since 2013), and I served many times on the PCs of CADE, IJCAR, RTA, LPAR, and several other conferences in the field. I have been CADE trustee from 2010-2011 and from 2014-2017.
The focus of my research in recent years has been on two important challenges in automated deduction: 1) how to validate that the complex techniques developed by the community produce correct results; and 2) how to exploit the power of big computer clusters. Although my work has targeted mainly SAT and QBF solving, these challenges are also important for first-order logic and beyond. My first paper on validation of SAT techniques was presented at IJCAR 2012 and my recent paper in this direction received a best paper award at CADE 17. I have been participating in the CADE and IJCAR conferences since 2012 and I was a CADE PC member in 2015 and 2017.
Researchers in the CADE community have created very powerful tools from Lingeling to Vampire to Z3. These tools are successful in industry as well. I am supportive of attracting paper submissions that describe how these tools can make a difference in solving relevant problems. Such papers can have a broad impact. I am also supportive of the requirement that experimental evaluations must be reproducible by the reviewers and the community at large. Although most CADE attendees come from Europe, I would like to stimulate participation from researchers in North America. Organizing CADE regularly in the US or Canada should therefore be continued. Maybe CADE could come back to Austin.
It is with sadness that we note the passing of Mike Gordon, one of the inventors of the Edinburgh LCF system and a central figure in the HOL community, on August 22 2017.
Obituary of the University of Cambridge Computer Laboratory.
Computer Theorem Proving is becoming a paradigm as well as a technological base for a new generation of educational software in science, technology, engineering and mathematics. The workshop brought together experts in automated deduction with experts in education in order to further clarify the shape of the new software generation and to discuss existing systems. This call is open for everyone, also those who did not participate in the workshop.
Topics include:
Important Dates:
For information about the submission process, see the workshop website.
The field of Symbolic Computation, and its implementation in Computer Algebra Systems, is concerned with the algorithmic determination of exact solutions to mathematical problems. More recent developments in the field of Satisfiability Checking are starting to tackle similar problems, through the use of Satisfiability Modulo Theory (SMT) solvers which exploit technology built for the Boolean SAT problem to other domains.
The two communities now share many central interests, but until recently there has been little interaction between them. Further, the lack of common or compatible interfaces is an obstacle to the fruitful combination of tools. Bridges between the communities in the form of common platforms and road-maps are needed to initiate exchange and support interaction. The aim of this special issue, along with the SC-square H2020 FETOPEN Coordination and Support Activity project, is to document progress, and share knowledge and experience across both communities.
The issue is open for submission and participation to everyone interested in the topics, whether they are members or associates of the SC-square project or not, and whether or not the contribution was discussed at the SC-square workshops.
Important Dates:
For information about the submission process, see the project website.
Certified Programs and Proofs (CPP) is an international forum on theoretical and practical topics in all areas, including computer science, mathematics, and education, that consider certification as an essential paradigm for their work. Certification here means formal, mechanized verification of some sort, preferably with production of independently checkable certificates.
Topics: Submissions in research areas related to formal certification of programs and proofs are welcome. The following is a suggested list of topics of interests to CPP. This is a non-exhaustive list and should be read as a guideline rather than a requirement.
Important Dates:
For information about the submission process, see the conference website.
The widespread use and increasing complexity of mission-critical and safety-critical systems at NASA and in the aerospace industry require advanced techniques that address these systems' specification, design, verification, validation, and certification requirements. The NASA Formal Methods Symposium (NFM) is a forum to foster collaboration between theoreticians and practitioners from NASA, academia, and industry. NFM's goals are to identify challenges and to provide solutions for achieving assurance for such critical systems.
Topics include:
Important Dates:
For information about the submission process, see the conference website.
Writing down detailed computational steps is not the only way of programming. The alternative, being used increasingly in practice, is to start by writing down the desired properties of the result. The computational steps are then (semi-)automatically derived from these higher-level specifications. Examples of this declarative style include functional and logic programming, program transformation and re-writing, and extracting programs from proofs of their correctness.
FLOPS aims to bring together practitioners, researchers and implementors of the declarative programming, to discuss mutually interesting results and common problems: theoretical advances, their implementations in language systems and tools, and applications of these systems in practice. The scope includes all aspects of the design, semantics, theory, applications, implementations, and teaching of declarative programming. FLOPS specifically aims to promote cross-fertilization between theory and practice and among different styles of declarative programming.
Topics include:
Important Dates:
For information about the submission process, see the conference website.
FSCD covers all aspects of formal structures for computation and deduction from theoretical foundations to applications. Building on two communities, RTA (Rewriting Techniques and Applications) and TLCA (Typed Lambda Calculi and Applications), FSCD embraces their core topics and broadens their scope to closely related areas in logics, proof theory and new emerging models of computation such as quantum computing or homotopy type theory.
Topics include:
Important Dates:
For information about the submission process, see the conference website.
IJCAR is the premier international joint conference on all topics in automated reasoning. The IJCAR technical program will consist of presentations of high-quality original research papers, system descriptions, and invited talks.
IJCAR 2018 takes place as part of FLoC 2018 and is the merger of leading events in automated reasoning:
Topics include:
Important Dates (provisional):
For information about the submission process, see the conference website.
CAV 2018 is the 30th in a series dedicated to the advancement of the theory and practice of computer-aided formal analysis methods for hardware and software systems. The conference covers the spectrum from theoretical results to concrete applications, with an emphasis on practical verification tools and the algorithms and techniques that are needed for their implementation. CAV considers it vital to continue spurring advances in hardware and software verification while expanding to new domains such as machine learning, autonomous systems, and computer security. The proceedings of the conference will be published in the Springer-Verlag Lecture Notes in Computer Science series. A selection of papers is expected to be invited to a special issue of Formal Methods in System Design and the Journal of the ACM.
Topics include:
Important Dates:
For information about the submission process, see the conference website.
FM 2018 is the latest in a series of symposia organized by Formal Methods Europe, an independent association that encourages the use of, and research on, formal methods for the engineering of computer-based systems and software. The symposia have been notably successful in bringing together researchers and industrial users around a programme of original papers on research and industrial experience, workshops, tutorials, reports on tools, projects, and ongoing doctoral work. FM 2018 will take place in Oxford, UK, 15-17 July 2018 as part of FLoC 2018, the Federated Logic Conferences.
FM 2018 will highlight the development and application of formal methods in a wide range of domains including software and integrated computer-based systems. In the latter field, cyber-physical systems, systems-of-systems, human-computer interaction, manufacturing, sustainability, power, transport, cities, healthcare, and biology are of particular interest. We also welcome papers on experiences of formal methods in industry, and on the design and validation of formal methods tools.
The broad topics of interest for FM 2018 include, but are not limited to:
Important Dates:
For information about the submission process, see the conference website.
Over the last decade, the boundaries between computer system components, such as hardware, software, firmware, middleware, and applications, have blurred. This evolution in system design and development practices led in 2014 to a change in the title and scope of the MEMOCODE conference from its original focus on hardware/software co-design to its new focus on formal methods and models for developing computer systems and their components. MEMOCODE's objective is to emphasize the importance of models and methodologies in correct system design and development, and to bring together researchers and industry practitioners interested in all aspects of computer system development, to exchange ideas, research results and lessons learned.
MEMOCODE'17 will be collocated with FMCAD'17, the 17th conference on Formal Methods in Computer-Aided Design, October 2-6, 2017. MEMOCODE'17 and FMCAD'17 will have joint tutorials on October 2.
For information about registration, see the registration website.
FMCAD 2017 is the seventeenth in a series of conferences on the theory and applications of formal methods in hardware and system verification. FMCAD provides a leading forum to researchers in academia and industry for presenting and discussing ground-breaking methods, technologies, theoretical results, and tools for reasoning formally about computing systems. FMCAD covers formal aspects of computer-aided system design including verification, specification, synthesis, and testing.
The program comprises presentations of 25 regular papers and 4 tool papers, 3 tutorials and 2 keynotes, a student forum, the Hardware Model Checking Competition, and a symposium in memoriam Helmut Veith.
Important Dates:
For information about registration, see the conference website.
PPDP 2017 is a forum that brings together researchers from the declarative programming communities, including those working in the functional, logic, answer-set, and constraint programming paradigms. The goal is to stimulate research in the use of logical formalisms and methods for analyzing, performing, specifying, and reasoning about computations, including mechanisms for concurrency, security, static analysis, and verification.
For information about registration, see the conference website.
The aim of the LOPSTR series is to stimulate and promote international research and collaboration on logic-based program development. LOPSTR is open to contributions in logic-based program development in any language paradigm. LOPSTR has a reputation for being a lively, friendly forum for presenting and discussing work in progress. Formal proceedings are produced only after the symposium so that authors can incorporate this feedback in the published papers.
For information about registration, see the conference website.
The 3rd Global Conference on Artificial Intelligence (GCAI 2017) will be held in Miami, USA, at the Courtyard Marriott hotel in Coconut Grove, 18-22 October 2017. The conference, which addresses all aspects of artificial intelligence, is being organized by LRG and the University of Miami. The program chairs are Christoph Benzmüller, Christine Lisetti and Martin Theobald. The conference chair is Geoff Sutcliffe.
Important Dates:
For information about registration, see the conference website.
HVC is an annual conference dedicated to advancing the state-of the art and state-of-the-practice in verification and testing. At the conference, researchers and practitioners from academia and industry network, share ideas, and ponder the future directions of testing and verification for hardware, software, and complex hybrid systems.
The common goal of the conference topics and participants is to ensure the correct functionality and performance of complex systems. HVC is the only conference that brings together experts from all verification and testing sub-fields, thereby encouraging the migration of methods and ideas among domains.
For information about registration, see the conference website.
The last installment of AsubL (Algebra and Substructural Logics) took place in Melbourne in December 2014. AsubL Take 6 will take place in Cagliari, from the 11th to the 13th of June, 2018, as a workshop in the framework of SYSMICS: SYntax meets Semantics: Methods, Interactions, and Connections in Substructural logics. Further information concerning the webpage, the venue, a tentative programme, a list of invited speakers, and a call for papers will be circulated presently. Following the informality tradition that characterised all past editions of AsubL, there will be no officially appointed scientific committee or organising committee. Potential participants, however, can contact Francesco Paoli or Antonio Ledda for information.
Safety-critical computers increasingly affect nearly every aspect of our lives. Computers control the planes we fly on, monitor our health in hospitals and do our work in hazardous environments. Computers with software deficiencies have resulted in catastrophic failures. The goal of formal verification is to to improve the safety and reliability of such hardware and software systems.
Formal Verification is the study of algorithms and structures applicable to the verification of hardware and software designs. It draws upon ideas and results from logic, graph theory, and automata theory, and combines theoretical and experimental aspects. While 30 years ago this was a subject of academic interest only, today, many companies use formal verification as an integral part of the development process.
The IIAS Winter School on Formal Verification would bring together several leading researchers to cover the mathematicall and algorithmic foundations of the field, as well as to discuss its application in industry, and its impact on related areas in computer science.
Confirmed speakers of the winter school:
Important Dates:
For information about registration, see the registration website.
We are looking to fill two permanent (subject to a probation period) roles in the broad area of employing reasoning-based techniques directly to program analysis for security properties, or to the verification of security-related protocols or algorithms. The focus on reasoning-based methods is targeted to complement our world-leading status in automated reasoning. The two positions reflect our desire to establish a new research area.
For full details and how to apply see here (the closing date is 30th September). For any questions please contact Andrei Voronkov and Giles Reger.
(For non-UK readers: the position of Lecturer corresponds to Assistant Professor, but note that this is a tenured position.)
Computer Aided Verification(succeeding Helmut Veith) at TU Wien
The TU Wien (Vienna University of Technology) invites applications for a full professorship at the Faculty of Informatics. The position is affiliated to the Institute of Information Systems. The candidate will become the head of the already existing and valid established research group Formal Methods in Systems Engineering, previously headed by Helmut Veith. The estimated starting date is October 1, 2018.
Application deadline is October 16, 2017. Further details on the position and requirements.
We are offering a PhD position on the integration of automated provers in proof assistants at the Laboratory on Specification and Verification (LSV) of the University Paris Saclay, supervised by Frederic Blanqui and Guillaume Burel.
To widen their use, proof assistants needs more automation. This can be performed by calling external automated theorem provers. Centered around Dedukti, a proof checker for the universal logical framework Lambda-Pi-calculus modulo theory, the objective is to design a proof environment that is able to call external provers to build part of the proof. The global architecture must emphasize the need to have a correct and exhaustive proof once the portions proved externally are glued together. From Dedukti to external provers, proof obligations in the Lambda-Pi-calculus modulo theory must be passed in an efficient way, either by encoding them or by extending the external prover to accept them. Reciprocally, proofs or proof traces produced by these tools needs to be reconstructed back into Dedukti.
Starting in October 2017, the programming languages group at University of Freiburg, Germany, has an opening for a research assistant to work with Prof. Dr. Peter Thiemann. This position can be filled with a graduate working towards a PhD or with a PostDoc and it involves a light amount of teaching. We welcome applications of either kind.
Research
The overall research theme of the group is to explore the boundaries
of static and dynamic checking of program properties.
We are working in the context of JavaScript, Haskell, OCaml, Scala, and admit the occasional excursion to Java and Go. We collaborate with leading researchers worldwide. Check our research webpage or DBLP publication profile for more information.
Requirements
Job Details and Application
The salary is according to the TV-L E13 scale of German public service.
The university of Freiburg aims at increasing the number of female employees and thus especially welcomes applications of female candidates.
Applications of disabled candidates will be given priority, depending on their suitability.
Please send your application in PDF format by email to the leader of the programming languages group, Prof. Dr. Peter Thiemann. Applications will be considered until the position is filled.
Informal enquiries about the position may also be sent to Prof. Dr. Peter Thiemann (web page)
The Chair MAIS at TU Darmstadt, led by Heiko Mantel, is offering multiple Postdoc and Ph.D. positions. We are looking for researchers who are interested in addressing foundational problems that will be of practical relevance or in addressing practical problems based on formal methods. The research focus shall be on software security, concurrency, or their combination.
The research focus shall be on one of the following topics:
Your research shall be based on solid theoretical foundations and could result, e.g., in foundational insights, in program analysis and transformation techniques, in tools that are reliable and efficient, in instructive case studies, or in verified critical software systems.
For more information about the positions, about the four research topics and about how to apply, see this web page.