Flyer
Program
INTERNATIONAL SUMMER SCHOOL ON COMPUTATIONAL LOGIC
In the frame of the project ARC
Automated Reasoning in the Class
Linz, Austria
4 – 8 July 2022
Co-organized by:
Johannes Kepler University, Linz, Austria,
West University of Timisoara, Romania,
RWTH Aachen University, Germany,
Eszterhazy Karoly Catholic University, Hungary,
University of Lorraine, France
SCOPE:
The goal of the summer school is that students to teach Computational Logic based on the ARC book (Computational Logic: A Practical Approach) produced in the ARC project and to use the tools developed in Theorema, Coq, Satisfiability Modulo Theories, and SATisfiability solvers in practical exercises based on Problem Based Learning principles.
PARTICIPANTS and FUNDING:
The school is open to students of all levels: Bachelor, Master’, and PhD. For a limited number of nonlocal participants we offer funding support of 290 Euro for subsistence and 180 to 275 for transport (depending on the distance).
VENUE:
Johannes Kepler University,
Research Institute for Symbolic Computation,
Science Park, Altenbergerstrasse 69, 4040 Linz, Austria
https://www.jku.at/campus/der-jku-campus/gebaeude/science-park-2
STRUCTURE:
There will be 5 full days of courses.
KEYNOTE PROFESSORS AND COURSES SUMMARY:
TUDOR JEBELEAN (Johannes Kepler University, Linz, Austria) – will present the basic notions of Mathematical Logic, an overview of the main automatic proof methods, and the main principles of program verification. He will use exercises based mainly on the Theorema system.
GABOR KUSPER (Eszterhazy Karoly Catolic University, Eger, Hungary) – will give an intensive training of SAT / SMT solver algorithms, and an intensive training of using SAT / SMT solvers. The first part introduces well-known algorithms, like DP, DPLL, CDCL, and less well-known ones like CSFLOC. This part covers also the lazy data structures and look-ahead heuristics used by SAT / SMT solvers. The participants will also implement a naive DPLL. The second part teaches how to use SAT / SMT solvers, how to state a problem as SAT / SMT problem, how to use them for theorem proving, how to use them to check software security conditions.
ERIKA ABRAHAM (RWTH Aachen University, Germany) – building upon the training given by Gabor Kusper, this training will focus in a first module on SMT solving techniques for arithmetic problems, using under others decision procedures that are rooted in computer algebra (virtual substitution, cylindrical algebraic decomposition, Groebner bases, subtropical satisfiability, etc.). In a second module, will discuss how to encode different problems logically, such that SMT solving can be used for their solution. Application examples will stem from verification and from planning.
ISABELA DRAMNESC (West University of Timisoara, Romania) – presenting techniques for algorithm synthesis on lists, on binary trees, how to extract different algorithms from proofs, how to explore a theory and concrete exercises by using the Problem Based Learning principles of teaching.
SORIN STRATULAT (University of Lorraine, France) – will give an intensive and concentrated version of the training course in Coq, to recall: Introduction, programming with natural numbers and lists in Coq, propositions and predicates, making proofs in Coq, inductive data types and inductive properties. A strong accent is put on making proofs in Coq and on certifying algorithms issued from the synthesis method based on Theorema.
DEADLINES
28 February 2022 – early application submissions (for funding)
15 March 2022 – late application submissions (no funding)
30 March 2022 – notification of acceptance/rejection
APPLICATIONS should contain a CV and a motivation letter (in which you should mention about your knowledge on Mathematical Logic and Automated Reasoning) and should be submitted to the EasyChair platform
https://easychair.org/conferences/?conf=arc2022
The number of applications which will be accepted for funding is restricted to 16.
Funding for selected participants: 290 Euro for subsistence and 180 to 275 for transport (depending on the distance).
ORGANIZING COMMITTEE:
Tudor Jebelean, Austria (chair)
Isabela Dramnesc, Romania (chair)
CERTIFICATE:
Participants will receive an attendance certificate indicating the number of hours of courses (equivalent to 3 ECTS credits).
CONTACT:
Photos from the event
