Seminars Learning Theorem Proving from Scratch Cezary Kaliszyk 2019/02/26 On the benefit of unsound rules: Henkin quantifiers and beyond Matthias Baaz 2019/02/26 Specification Verification of Hoare's Quicksort Algorithm in CafeOBJ Kokichi Futatsugi 2019/01/10 Blockchain for Asset Reuse Arnold Beckmann 2019/01/10 Automating Proof Terms in Term Rewriting Aart Middeldorp 2018/09/20 Dataset Diversity: A New Approach to Dependable Machine Learning Software Shin Nakajima (National Institute of Informatics, Tokyo) 2017/12/15 Provably Total NP Search Problems of Bounded Arithmetic and beyond Professor Arnold Beckmann 2017/09/15 Arithmetic universes as generalized point-free spaces Steve Vickers 2017/04/17 Unsound inferences make proofs shorter Matthias Baaz 2016/12/06 Invariance axioms for realizability Helmut Schwichtenberg 2016/08/25 Variations on the Higman's Lemma Marco Benini 2016/08/08 Models, Over-approximations and Robustness Eugenio Moggi (University of Genova) 2016/08/05 LECTURE 3: Models, Over-approximations and Robustness Eugenio Moggi 2016/08/05 Hybrid System Trajectories as Partial Continuous Maps Speaker: Eugenio Moggi (University of Genova) 2016/08/04 LECTURE 2: Hybrid System Trajectories as Partial Continuous Maps Eugenio Moggi 2016/08/04 LECTURE 1: Categories of Classes for Collection Types Eugenio Moggi 2016/08/02 Categories of Classes for Collection Types Eugenio Moggi (University of Genova) 2016/08/02 Random Graphs, First-Order Logic, and AC^0 Circuits Yijia Chen 2016/07/12 FORT 0.2: Confluence Properties on Open Terms in the First-Order Theory of Rewriting Aart Middeldorp 2016/07/12 Logical Omniscience and Deductive Rationality Ren-June Wang 2016/07/07 Computably Enumerable Structures: Domain dependency Bakhadyr Khoussainov 2016/06/20 On Some General Methods of Proving Decidability or Undecidability Hsing-chien Tsai 2015/10/06 Toward a Rewriting-based Semantics of Clock Constraint Specification Language and its Applications Zhang Min 2015/08/27 A Maude environment for CafeOBJ Adrian Riesco Rodriguez 2015/08/27 Real numbers and computers Norbert Müller 2015/08/25 Verification of Real-World Security Protocols in CafeOBJ: A Case Study of PACE Dominik Klein 2015/05/26 Digit Spaces - Topological Foundations Dieter Spreen 2015/05/07 Generic proof scores for the generate & check method in CafeOBJ Kokichi Futatsugi 2015/02/26 CDSChecker: Checking Concurrent Data Structures Written with C/C++ Atomics Brian Demsky, University of California Irvine 2015/01/09 Weighted Automata Theory for Complexity Analysis of Rewrite Systems Georg Moser 2015/01/08 An update for the Constructor-based Inductive Theorem Prover (CITP) Daniel Gaina 2014/11/20 Towards a Science of Computing Prof. Robert Kowalski 2014/10/28 Counterexample-guided Design of Property-based Dynamic Software Updates Zhang Min 2014/10/15 Relational lattices Tadeusz Litak 2014/09/18 Tomorrow belongs to deviant intuitionistic modalities Tadeusz Litak 2014/09/17 An update for CITP Daniel Gaina 2014/08/28 Malware techniques and its pushdown model checking Nguyen Minh Hai 2014/08/22 Liveness properties in CafeOBJ Norbert Preining 2014/08/07 Fissile Type Analysis: Modular Checking of Almost Everywhere Invariants Bor-Yuh Evan Chang 2014/08/06 Termination Analysis for Term Rewriting Nao Hirokawa 2014/08/04 A Realizability Model for Type Theory Keiko Nakata 2014/07/07 Generate & Check Method in CafeOBJ Revised Kokichi Futatsugi 2014/07/03 Bi-Intuitionistic Modal Logic and Hypergraphs Dr. John Stell 2014/06/27 Point-free foundations of Mathematics Dr. Marco Benini 2014/05/22 40 Years of Formal Methods Some obstacles and some possibilities Dines Bjorner 2014/04/18 Extracting programs from proofs Prof. Dr. Helmut Schwichtenberg 2014/03/07 A theory of computable functionals Prof. Dr. Helmut Schwichtenberg 2014/03/06 Computing with partial continuous functionals Prof. Dr. Helmut Schwichtenberg 2014/03/05 Bounded variable logic, parameterized logarithmic space, and Savitch's theorem Yijia Chen 2014/01/23 Parity Games and Resolution Arnold Beckmann 2014/01/23