Argo Seminar: Announcements
Click here for Serbian version.  Kliknuti ovde za verziju na srpskom jeziku.
Argo seminar is a regular seminar of the Argo group. Main fields discussed are Automated Reasoning and Applications, Theoretical Computer Science, Artificial Intelligence and Data Mining. The seminar is dedicated mainly to PhD students in Computer Science. One meeting typically consists of two lectures: a tutorial one (where known results on one specific topic are presented) and a research one (where original research work is presented).
Meetings take place once in two weeks, usually on Thursday at 6:00PM, in the premises of the Faculty of Mathematics in Studentski trg street, classroom 718.
Seminar secretary: Vesna Marinković
If you are interested in receiving information on the seminar and lecture announcements, please send an email to Vesna Marinković or Predrag Janičić .
11.10.2018.

Pavle Subotic, Amazon
Title: Debugging Large Scale Logic ProgramsAbstract:
Logic programming languages such as Datalog have become popular as Domain Specific Languages (DSLs) for solving largescale problems, in particular, static program analysis including pointsto analysis and network analysis. Logic programs that process largescale data are, however, difficult to debug. In the database community, data provenance techniques have been proposed that could address the Declarative Debugging Challenge for largescale inputs. Unfortunately, the current stateoftheart approaches for dataprovenance cannot cope with big data.
In this talk, I discuss a novel provenance evaluation strategy for debugging Datalog programs. The provenance evaluation strategy relies on a new provenance lattice which incorporates proof annotations. We define a new fixedpoint semantics for seminaive evaluation to compute with the augmented lattice, and propose a provenance query mechanism to constructs partial minimal height proofs for tuples.
29.3.2018.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Title: The Univalence Axiom in Dependent Type TheoryAbstract:
We give an introduction to the theory with dependent types and inductive equality, and discuss the new Univalence Axiom recently proposed by Voevodsky.
28.12.2017.

Aleksandar Zeljić, Uppsala University
Title: A ModelConstructing Approach to Solving BitVector ConstraintsAbstract:
The ModelConstructing Satisfiability Calculus (mcSAT) is a recently proposed generalization of the DPLL(T) framework for SMT. Unlike most DPLL(T)based SMT solvers, which carry out conflictdriven learning only on the propositional level, mcSAT calculi can also synthesize new theory literals during learning, resulting in a simple yet very flexible framework for designing efficient decision procedures. In this talk, we present an instantiation of the mcSAT calculus for the theory of fixedsize bitvectors, based on tailormade conflictdriven learning that exploits both propositional and arithmetic properties of bitvector operations. In our approach, bitvectors are firstorder citizens and unnecessary bitblasting is avoided altogether.
23.3.2017.

Julien Narboux, University of Strasbourg
Title: GeoCoq, foundations of geometry formalized in CoqAbstract:
In this talk we will give an overview of the GeoCoq library developed by our team in Strasbourg ( http://geocoq.github.io/GeoCoq/ ). GeoCoq library contains a systematic development of geometry from Tarski’s or Hilbert’s axioms. From these axiom systems, we formalized the culminating results of both Tarski, Schwabhäuser, Szmielew, Metamathematische Methoden in der Geometrie and Hilbert, Foundations of Geometry, namely the arithmetization of geometry. This connection between synthetic geometry and algebra, allows us to use algebraic methods for automated deduction in geometry in a synthetic setting. We have also studied the formal proof of the equivalence between 34 versions of the parallel postulates. We work in neutral geometry in an intuitionistic setting and study the impact of different continuity properties on the equivalence proofs. This result in four groups of postulates, which are all equivalent assuming Archimedes’ axiom but distinct, in constructive logic without Archimedes’ axiom. Finally, I will report our ongoing work toward the formalization of Euclid’s Elements proposition in Coq.
22.09.2016.

Tetsuo Ida, University of Tsukuba
Title: Computational Origami System EosAbstract:
I will talk about a computational origami system called Eos (eorigami system) that we have developed over the years. I will cover briefly the motivation, the development process, underlying theories and the functionalities of Eos. During the talk, I would like to emphasize the aspects of Eos as a tool for interactive origami construction, and the geometric theorem prover of origami theorems. 
Mircea Marin, West University of Timisoara
Title: Solving, Reasoning, and Programming in Common LogicAbstract:
Common Logic (CL) is an ISO standard for exchanging logicbased information in heterogeneous, open networks of computerbased systems. The representational requirements of knowledge in open networks led to some important changes of traditional firstorder logic: In CL, symbols (called names) do not have fixed arity (variable polyadicity), the language contains sequence variables that stand for finite sequences of terms, one and the same symbol can play the syntactic roles of both constant, function symbol and predicate (crosscategoricity), terms can be applied to other terms, and the language is typefree. These adaptations pose new challenges to the design and development of reasoning tools for Common Logic. Sharing and reasoning upon knowledge represented in CL require equation solving over terms of this language. We succeeded to identify computationally wellbehaved fragments of such solving problems. In this talk, I will present the fragments and solving methods discovered by us, and indicate how they can influence reasoning in CL and transformations of CL expressions.
24.03.2016.

Pavle Subotić, University College London
Title: Synthesizing Analyzers from DatalogAbstract:
Among the reasons for the slow industrial adoption of static code analysis is the lack of sufficient customizability and scalability available in tools. Recently, the use of Datalog, has had a resurgence in several computer science communities, particularly, in the area of program analysis where tools such as muZ, LogicBlox and bddbddb have shown great promise. In these tools, Datalog acts as a domain specific language to express custom program analyses concisely, reducing the complexity of developing program analyzers. The drawback, however, is that analyses specified in Datalog typically experience reduced performance compared to manually implemented tools. To close the performance gap, we have developed a tool called /Soufflè/ that overcomes the performance limitations of standard Datalog evaluation by performing an efficient synthesis of Datalog to executable C++ programs. As a result, /Soufflè/ is able to perform analyses onpar with stateoftheart manual tools (e.g., performs a pointsto analysis on OpenJDK in 35 seconds) while retaining the advantages of employing a domain specific language for expressing static analyses. In this talk, I will present an overview of the /Soufflè/ framework, focusing on one of its key optimizations, namely, /Optimal Index Generation/, which it performs to efficiently synthesize Datalog to C++.
07.05.2015.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Title: Coquand's site semantics of coherent logicAbstract:
We introduce socalled site models of coherent theories, due to Coquand. We prove completeness and discuss the status of formulas that are true in the site model of a coherent theory.
30.04.2015.

Bojan Petrović, Haklab Belgrade
Informal VerificationAbstract:
A Coq workshop based on "Software Foundations" course at University of Pennsylvania was held in Hacklab Belgrade hackerspace from June 2012 to December 2013. The core of the course is the study of operational semantics and type systems of programming languages, together with an introduction to formal reasoning about functional and imperative programs. We will present an overview of the "Software Foundations" course, provide some basic information on Coq proof assistant, and highlight some of the experiences gained through teaching in an informal, noninstitutional setting.
22.07.2014.
24.07.2014.

Marc Bezem, Institute for Informatics, University of Bergen, Norway
Title: Homotopy Type TheoryAbstract:
Homotopy type theory is a new branch of mathematics that combines aspects of several different fields in a surprising way. It is based on a recently discovered connection between homotopy theory and type theory. Homotopy theory is an outgrowth of algebraic topology and homological algebra, with relationships to higher category theory; while type theory is a branch of mathematical logic and theoretical computer science. Homotopy type theory also brings new ideas into the very foundation of mathematics. For example, there is Voevodsky's subtle and beautiful Univalence Axiom. The univalence axiom implies, in particular, that isomorphic structures can be identified, a principle that mathematicians have been happily using on workdays, despite its incompatibility with the "official" doctrines of conventional foundations. In the seminar we will focus on type theory for formalizing mathematics and work through (parts of) the HoTT book, freely available from: http://ufias2012.wikispaces.com/The+book
02.07.2014.

Sana Stojanović, Faculty of Mathematics, University of Belgrade
Title: A Vernacular for Coherent Logic and Automated Generation of Machine Verifiable and Readable ProofsAbstract:
We will present our framework for automated generation of proofs from the book "Metamathematische Methoden in der Geometrie" (by Wolfram Schwabhauser, Wanda Szmielew, and Alfred Tarski) using resolution theorem provers and a coherent logic theorem prover. Also, we will present a simple proof representation that we developed within coherent logic. This proof representation can be used for generation of proofs in different proof assistants (Isar and Coq). 
Mirko Stojadinović, Faculty of Mathematics, University of Belgrade
Title: Instancebased Selection of CSP Solvers using Short TrainingAbstract:
Title: Air Traffic Controller Shift Scheduling by Reduction to CSP, SAT and SATrelated Problems
Many different approaches for solving Constraint Satisfaction Problems (CSP) (and related Constraint Optimization Problems (COP)) exist. However, there is no single solver that performs well on all classes of problems and many portfolio approaches for selecting a suitable solver based on simple syntactic features of the input CSP instance are developed. We will present a portfolio method for CSP based on knearest neighbors method. Unlike other existing portfolio approaches for CSP, our methodology is based on training with very short timeouts, thus significantly reducing overall training time. Still, thorough evaluation has been performed on large publicly available corpora and our portfolio method gives good results. The method improves upon the efficiency of single stateoftheart tools used in comparison, and is comparable to classical methods that use long timeout during the training phase.Abstract:
We will present our experience in solving Air Traffic Controller Shift Scheduling Problem. We will give a formal definition of this optimization problem and introduce three encodings. The encodings make possible to formulate a very wide set of different scheduling requirements. The problem is solved by using SAT, MaxSAT, PB, SMT, CSP and ILP solvers. In combination with these solvers, three different optimization techniques will be presented, a basic technique and its two modifications. The modifications use local search to modify some parts of the initial solution. Results indicate that SATrelated approaches outperform other solving methods used and that one of the introduced techniques which uses local search can significantly outperform the basic technique. We have successfully used these approaches to make shift schedules for one air traffic control center.
13.03.2014.

Aleksandar Zeljic, Department of Information Technology, Uppsala University, Sweden
Title: Approximations for Model ConstructionAbstract:
We consider the problem of efficiently computing models for satisfiable constraints, in the presence of complex background theories such as floatingpoint arithmetic (FPA). Model construction has various applications, for instance the automatic generation of test inputs. It is wellknown that naive encoding of constraints into simpler theories (for instance, bitvectors or propositional logic) can lead to a drastic increase in size, and be unsatisfactory in terms of memory and runtime needed fo