Wednesday 8th February 2023,16:00
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Jaroslav Bendík, Certora, Israel
Formal Verification of Smart Contracts using Certora Prover
Ethereum Smart Contracts become a widely adopted technology to build Decentralized Financial Applications (DeFis) and as such,
they already hold 200 billion USDs. Consequently, bugs in smart contracts can be exploited by malicious users and
can lead to losses at the scale of millions or even billions of USDs. To prevent such situations from happening,
there has been a growing interest in developing scalable formal verification techniques for this domain.
In this talk, we will specifically focus on the architecture of the Certora VerificationTool,
i.e. an industrial standard automated prover technology to verify smart contracts.
Besides a brief overview of the overall tool architecture, we will focus mainly on the SMTbased subroutines,
including features such as domainspecific CEGAR methodology, distributed solverportfolio approach,
or techniques to share and exploit information between individual SMT solvers.

Wednesday 25th January 2023,16:30
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Adrian de Lon, Hausdorff Center for Mathematics, Bonn
What is Natural Proof Checking?
A “Natural” proof assistant is one that aims for formalizations that are close to ordinary mathematical texts. I will briefly explain the motivations behind the natural proof assistant Naproche and then talk about its implementation and the overall status of the project. I will conclude with a demo of Naproche (plus answering questions), probably using my WIP formalization of Tarskian geometry.

Wednesday 18th January 2023,16:00
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Barbora Hudcova, CIIRC, CTU, Prague
Studying Cellular Automata Dynamics via Statistical Physics
In this talk, I will share what I learned during my 3monthlong internship at the statistical physics group in EPFL, Lausanne. I will introduce the belief propagation algorithm and explain how it can be used to analyze the dynamics of discrete systems. I will discuss how this relates to my main field of research: studying complexity of discrete systems.

Wednesday 4th January 2023,17:00
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Probabilistic constructions in groups
We know that certain objects exist even though we can't
provide a single example. One way we establish such knowledge is with
the probabilistic method: we show that a randomly selected object has
the desired property with nonzero probability. I'll present
probabilistic proofs in group theory. I'll mostly talk about maps into
finite groups that preserve certain properties (such as disjointness,
nonmembership, nonconjugacy).

Wednesday 4th January 2023,15:30
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

PyLogic  Pythonic ITP
Softtyped, even without hard distinction between formulas and objects. Kept simple stupid, yet expressive and vertisile. Logic can mimic e.g. natural deductionstyle, or skolemization & resolution. Core written in pure Python but extensible with external ATPs. We will discuss the logical foundations, design choices, future plans, and how / if they differ from existing ITPs.

Friday 18th November 2022,11:30
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

On hybrid commonsense question answering: research questions for adding machine learning to a logicbased framework
We are building logicbased components of a hybrid system for natural language commonsense question answering with explanations: a commonsense knowledge base, a first order reasoner extended with confidences and default logic, a semantic parser for English. The main upcoming tasks are finding different ways to integrate machine learning into all components of the system. Learning to guide proof search is one of the targets, but machine learning could be also used for improving both the knowledge base and semantic parsing. The talk will give an overview of the current system, briefly describe other similar projects and outline several research questions and ideas for applying machine learning in this framework.

Wednesday 19th June 2019,15:00pm
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

When is a formula program invariant?
Program invariants play an important useful role in understanding
programs as well as verifying properties
about them. There are many ways to obtain program
invariantsautomatically, semiautomatically
or they could be provided by a programmer as a part of a specification
of the program or as annotations.
The problem of determining whether a proposed formula is an invariant is
undecidable. In this talk, methods
are proposed to determine when in certain cases, formulas expressed in
various logical theories can be determined
to be invariant. If a formula is indeed an invariant, a
saturation based procedure for
strengthening the formula to generate
inductive invariants are explored. This approach is contrasted
with property directed reachability approach toward for program
analysis.

Tuesday 11th June 2019,11:45am
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Adding set theory to E prover
TBA

Tuesday 4th June 2019,11:45am
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Label invariant neural networks for formula embeddings.
I will talk about convolutional graph neural networks used for reinforcement learning with leanCoP.

Friday 24th May 2019,14:00pm
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Karel Chvalovsky, CIIRC, CTU, Prague
Neural representations of formulae
In this talk, I briefly present various approaches how to
represent a formula using neural networks. This includes
representations where a formula is a sequence of symbols, a tree,
and a part of a more involved graph structure.

Friday 24th May 2019,11:45am
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Shawn Wang, CIIRC, CTU, Prague
BLEU: a Method for Automatic Evaluation of Machine Translation
In this talk, I will explain what is the BLEU (Bilingual Evaluation Understudy) rate used in machine translation evaluations and how it is useful for our informal2formal experiments.

Friday 11th January 2019,12:00pm
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Curriculum Learning for Connectionbased Theorem Proving
In this informal lecture, I present latest developments of curriculum learning of theorem proving in the LeanCoP setting.
I present a simple reinforcement learning system based on proximal policy optimization (PPO) that was trained to guide the proof search of LeanCoP ATP.
We first trained the system on simple arithmetic formulae (in Robinson arithmetic),
which successfully generalized from the proof of a single multiplication (1*1=1) to additions/multiplications with arbitrarily large numbers.
We are working to extend these results to more complex arithmetic formulae and then  hopefully  to more complex problem domains as well.

Friday 5th October 2018, 2:30pm
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

Towards Smarter MACEstyle Model Finders
Finite model finders represent a powerful tool for deciding problems with the finite model property,
such as the BernaysSchoenfinkel fragment (EPR). Further, finite model finders provide useful information for countersatisfiable conjectures.
In this talk, I will describe several novel techniques in a finite modelfinder based on the translation to SAT, referred to as the MACEstyle approach.
The proposed approach is driven by counterexample abstraction refinement (CEGAR),
which has proven to be a powerful tool in the context of quantifiers in satisfiability modulo theories (SMT) and quantified Boolean formulas (QBF).
One weakness of CEGARbased approaches is that certain amount of luck is required in order to guess the right model,
because the solver always operates on incomplete information about the formula.
To tackle this issue, the model finder is enhanced with a machine learning algorithm to improve the likelihood that the right model is encountered.
The implemented prototype based on the presented ideas shows highly promising results.

Tuesday 19th September 2017, 2:30pm
CIIRC building A, 6th floor, room A622 at Jugoslávských partyzánů 1580/3, Prague 6

CakeML is a functional programming language with a provencorrect compiler and runtime system. Ramana is one of the main developers of CakeML.

Thursday 22nd June 2017, 3:00pm
CIIRC building A, 6th floor, room A623 at Jugoslávských partyzánů 1580/3, Prague 6

Jet Engine Software
In this talk, I explain how computers control modern jet engines, and how they manage to keep them safe and reliable. I briefly explain how a jet engine works, before covering some basics about engine control hardware and software architecture. I then go on to talk about the software development processes that are typically employed.

Friday 16th June 2017, 2:30pm
CIIRC building A, 6th floor, room A623 at Jugoslávských partyzánů 1580/3, Prague 6


Friday 26th May 2017, 2:30pm
CIIRC building A, 6th floor, room A623 at Jugoslávských partyzánů 1580/3, Prague 6

"What I have been doing during my spring vacation in Prague"

Tuesday 27th December 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6

The mystery of QBF tautologies
A tautological clause is a clause which contains both a literal and its complement.
While in the classical setting of propositional and firstorder logic tautologies are harmless
(in the sense that they are always vacuously satisfied and thus can be safely discarded),
in the study of resolutionbased calculi for quantified boolean formulas (QBF)
we encounter tautologies which can be harmful (their generation is explicitly prohibited,
because they would make the calculus unsound), but also useful
(the longdistance resolution calculus gains exponential power over
Qresolution by allowing generation of certain tautologies). I will try to shed light
on this discrepancy through the lens of the translation of QBF to firstorder logic proposed
by Seidl et al. (2012). This should also motivate a discussion about the currently missing
local semantics of a clause within the context of QBF resolutionbased calculi.

Monday 14th November 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6


Monday 31st October 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6


Tuesday 25th October 2016, 12:45am
BLOX building 8th floor at Evropská 2785/11, Prague 6

Lifted Relational Neural Networks
We propose a method combining relationallogic representations with neural network learning. A general lifted architecture, possibly reflecting some background domain knowledge, is described through relational rules which may be handcrafted or learned. The relational ruleset serves as a template for unfolding possibly deep neural networks whose structures also reflect the structures of given training or testing relational examples. Different networks corresponding to different examples share their weights, which coevolve during training by stochastic gradient descent algorithm. The framework allows for hierarchical relational modeling constructs and learning of latent relational concepts through shared hidden layers weights corresponding to the rules. Discovery of notable relational concepts and experiments on 78 relational learning benchmarks demonstrate favorable performance of the method.

Thursday 14th July 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6


Monday 30th May 2016, 2:00pm
BLOX building 6th floor at Evropská 2785/11, Prague 6

Knot recognition by SAT and ATP

Friday 6th May 2016, 1:30pm
BLOX building 6th floor at Evropská 2785/11, Prague 6

Initial Experiments with Neural Networks using TensorFlow Framework

Friday 1st April 2016, 2:30pm
BLOX building 6th floor at Evropská 2785/11, Prague 6

Prover9 and Solving Open Problems Using Hints

Wednesday 9th March 2016, 11:00am
BLOX building 6th floor at Evropská 2785/11, Prague 6

Concept Matching Between Formal Libraries

Friday 4th March 2016, 11:00am
BLOX building 6th floor at Evropská 2785/11, Prague 6

Finding Finite Models in MultiSorted First Order Logic

Friday 19th February 2016, 2:30pm
BLOX building 6th floor at Evropská 2785/11, Prague 6


Monday 7th April 2014, 4:15pm
Room 112

Multiagent Planning by Iterative Negotiation over Distributed Planning Graphs  Part 2
Deterministic multiagent planning described by MASTRIPS
formalism requires mixture of coordination and synthesis of
local agents' plans. All agents' plans, as sequences of actions, can be
implicitly described by an appropriate generative structure. Having
all local plans of all participating agents described by such a structure
and having a merged process of such structures, we can induce a
global multiagent plan by successive elimination of unfeasible combinations
of local agents' plans.
In this paper, we propose use of Nondeterministic Finite StateMachines
(NFSs) as the generative structure for the plans and use of
wellknown process of intersection of NFSs to prune the plan spaces
towards globally feasible multiagent plan. Since the numbers of the
plans can be large we use iterative process of building of the NFSs
using a stateoftheart classical planner interleaved with the NFS intersecting
process. To show efficiency of the approach, we have evaluated
the algorithm on extensive number of planning problems from
Internation Planning Competition extended for multiagent planning.

Monday 24th March 2014, 4:15pm
Room 112

Multiagent Planning by Iterative Negotiation over Distributed Planning Graphs  Part 1
Deterministic multiagent planning described by MASTRIPS
formalism requires mixture of coordination and synthesis of
local agents' plans. All agents' plans, as sequences of actions, can be
implicitly described by an appropriate generative structure. Having
all local plans of all participating agents described by such a structure
and having a merged process of such structures, we can induce a
global multiagent plan by successive elimination of unfeasible combinations
of local agents' plans.
In this paper, we propose use of Nondeterministic Finite StateMachines
(NFSs) as the generative structure for the plans and use of
wellknown process of intersection of NFSs to prune the plan spaces
towards globally feasible multiagent plan. Since the numbers of the
plans can be large we use iterative process of building of the NFSs
using a stateoftheart classical planner interleaved with the NFS intersecting
process. To show efficiency of the approach, we have evaluated
the algorithm on extensive number of planning problems from
Internation Planning Competition extended for multiagent planning.

Monday 10th March 2014, 4:15pm
Room 112

Lemma mining over HOL Light
Large formal mathematical libraries consist of millions of atomic inference steps that give rise to a corresponding number of proved statements (lemmas). Analogously to the informal mathematical practice, only a tiny fraction of such statements is named and reused in later proofs by formal mathematicians. In this work, we suggest and implement criteria defining the estimated usefulness of the HOL Light lemmas for proving further theorems. We use these criteria to mine the large inference graph of all lemmas in the core HOL Light library, adding thousands of the best lemmas to the pool of named statements that can be reused in later proofs. The usefulness of the new lemmas is then evaluated by comparing the performance of automated proving of the core HOL Light theorems with and without such added lemmas.

Monday 18th November 2013, 4:05pm
Room 112

Undecidability of Consequence Relation in Full Nonassociative Lambek Calculus
We prove that the consequence relation in the Full Nonassociative Lambek calculus is undecidable. An encoding of the halting problem for 2tag systems using finitely many nonlogical axioms in the language {⋅,∨} will be presented. Therefore already the consequence relation in this fragment is undecidable. Moreover, the construction works even when the structural rules of exchange and contraction are added.

Monday 21st October 2013, 4:05pm
Room 112

Automated Generating of Hypotheses by Genetic Algorithms

Monday 7th October 2013, 4:15pm
Room 112

Automated Reasoning Service for HOL Light
HOL(y)Hammer is an AI/ATP service for formal (computerunderstandable) mathematics encoded in the HOL Light system, in particular for the users
of the large Flyspeck library. The service uses several automated reasoning systems combined with several premise selection
methods trained on previous Flyspeck proofs, to attack a new conjecture that uses the concepts defined in the Flyspeck library. The public online
incarnation of the service runs on a 48CPU server, currently employing
in parallel for each task 25 AI/ATP combinations and 4 decision procedures that contribute to its overall performance. The system is also
available for local installation by interested users, who can customize it for their own proof development. An Emacs interface allowing parallel
asynchronous queries to the service is also provided. The overall structure of the service is outlined, problems that arise are discussed, and an
initial account of using the system is given.

Monday 29th April 2013, 4:15pm
Room 112

General Bindings and AlphaEquivalence in Nominal Isabelle
Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover. It provides a proving infrastructure for reasoning about programming language calculi involving named bound variables (as opposed to deBruijn indices). In this paper we present an extension of Nominal Isabelle for dealing with general bindings, that means termconstructors where multiple variables are bound at once. Such general bindings are ubiquitous in programming language research and only very poorly supported with single binders, such as lambdaabstractions. Our extension includes new definitions of alphaequivalence and establishes automatically the reasoning infrastructure for alphaequated terms. We also prove strong induction principles that have the usual variable convention already built in.

Monday 18th March 2013, 4:15pm
Room 112


Monday 4th March 2013, 4:15pm
Room 112

Duality in STRIPS planning II
We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its precondition and delete list, one obtains for every STRIPS task its dual version, which has a solution if and only if the original does. This is proved by showing that the described transformation essentially turns progression (forward search) into regression (backward search) and vice versa.
The duality sheds new light on STRIPS planning by allowing a transfer of ideas from one search approach to the other. It can be used to construct new algorithms from old ones, or (equivalently) to obtain new benchmarks from existing ones. Experiments show that the dual versions of IPC benchmarks are in general quite difficult for modern planners. This may be seen as a new challenge. On the other hand, the cases where the dual versions are easier to solve demonstrate that the duality can also be made useful in practice.

Monday 18th February 2013, 4:15pm
Room 112

Duality in STRIPS planning I
We describe a duality mapping between STRIPS planning tasks. By exchanging the initial and goal conditions, taking their respective complements, and swapping for every action its precondition and delete list, one obtains for every STRIPS task its dual version, which has a solution if and only if the original does. This is proved by showing that the described transformation essentially turns progression (forward search) into regression (backward search) and vice versa.
The duality sheds new light on STRIPS planning by allowing a transfer of ideas from one search approach to the other. It can be used to construct new algorithms from old ones, or (equivalently) to obtain new benchmarks from existing ones. Experiments show that the dual versions of IPC benchmarks are in general quite difficult for modern planners. This may be seen as a new challenge. On the other hand, the cases where the dual versions are easier to solve demonstrate that the duality can also be made useful in practice.

Wednesday 2nd January 2013, 1:30pm
Room 112

Executing HOL Project in the Isabelle theorem prover
In Isabelle/HOL, code generation is understood as the transformation of a system of equational theorems into a program in a functional programming language with the same equational semantics. This guarantees partial correctness of generated programs.
This generic framework is instantiated for SML, OCaml and Haskell. The metatheory permits program and datatype refinement, i.e. the replacement of abstract algorithms and representations by efficient and executable programs and data structures . without endangering partial correctness.
On top of this, the scope of executable specifications can be extended by providing tools which produce suitable equational specifications from theories. An example is a predicate compiler which turns inductive specifications into equational ones, thus opening the world of functionallogic programming for code generation.
Additionally, we have provided Haskabelle which transforms a subset of Haskell to Isabelle/HOL theory text.

Monday 21st January 2013, 4:15pm
Room 112


Friday 21st December 2012, 4:00pm
Room 112

On Propositional QBF Expansions and QResolution
Over the years, proof systems for propositional satisfiability (SAT) have been extensively studied. Recently, proof systems for quantified Boolean formulas (QBFs) have also been gaining attention. Qresolution is a calculus enabling producing proofs from DPLLbased QBF solvers. While DPLL has become a dominating technique for SAT, QBF has been tackled by other complementary and competitive approaches. One of these approaches is based on expanding variables until the formula contains only one type of quantifier; upon which a SAT solver is invoked. This approach motivates the theoretical analysis carried out in this paper. We focus on a two phase proof system, which expands the formula in the first phase and applies propositional resolution in the second. Fragments of this proof system are defined and compared to Qresolution.

Monday 3rd December 2012, 4:15pm
Room 112

ATP over Flyspeck
The considerable mathematical knowledge encoded by the Flyspeck project is combined with external automated theorem provers (ATPs) and machinelearning premise selection methods trained on the proofs, producing an AI system capable of answering a wide range of mathematical queries automatically. The performance of this architecture is evaluated in a bootstrapping scenario emulating the development of Flyspeck from axioms to the last theorem, each time using only the previous theorems and proofs. It is shown that 39% of the 14185 theorems could be proved in a pushbutton mode (without any highlevel advice and user interaction) in 30 seconds of real time on a fourteenCPU workstation. The necessary work involves: (i) an implementation of sound translations of the HOL Light logic to ATP formalisms: untyped firstorder, polymorphic typed firstorder, and typed higherorder, (ii) export of the dependency information from HOL Light and ATP proofs for the machine learners, and (iii) choice of suitable representations and methods for learning from previous proofs, and their integration as advisors with HOL Light. This work is described and discussed here, and an initial analysis of the body of proofs that were found fully automatically is provided.

Monday 19th November 2012, 4:15pm
Room 112

Semantic guidance for unbounded symbolic reachability

Monday 5th November 2012, 4:15pm
Room 112

Scheduling with and without Z3
