Research in RiSE at MSR (abstract)

Harrsh: A Tool for Unied Reasoning about Symbolic-Heap Separation Logic (abstract)

Extending a Verified Simplex Algorithm (abstract)

ProofWatch Meets ENIGMA: First Experiments (abstract)

Influence of Variables Encoding and Symmetry Breaking on the Performance of Optimization Modulo Theories Tools Applied to Cloud Resource Selection (abstract)

Splitting a Logic Program Efficiently (abstract)

Verification, Testing, and Runtime Monitoring of Automotive Exhaust Emissions (abstract)

Function Summarization Modulo Theories (abstract)

Lookahead-Based SMT Solving (abstract)

Arrays Made Simpler: An Efficient, Scalable and Thorough Preprocessing (abstract)

Symmetry breaking in a new stable model search method (abstract)

On Disallowing Punctual Intervals in Reflexive Semantics of Halpern-Shoham Logic (abstract)

Towards Efficient Metaquery Generator (abstract)

Variations on the Classical Maximum-Flow Problem (abstract)

Two-variable First-Order Logic with Counting in Forests (abstract)

Completeness of Left Handed Kleene algebra via Cyclic Proofs (abstract)

A Verified Theorem Prover Backend Supported by a Monotonic Library (abstract)

Alternating Reachability Games with Behavioral and Revenue Objectives (abstract)

Polymorphic success types for Erlang (abstract)

Parse Condition: A Symbolic Encoding for LL(1) Parsing (abstract)

Loop Analysis by Quantification over Iterations (abstract)

Automatic Space Bound Analysis for Functional Programs with Garbage Collection (abstract)

Linear Tree Constraints (abstract)

When Are Two Gossips the Same? (abstract)

In Memory of Martin Hofmann (abstract)

Quasipolynomial Set-Based Symbolic Algorithms for Parity Games (abstract)

Evaluation of Domain Agnostic Approaches for Enumeration of Minimal Unsatisfiable Subsets (abstract)

SMTS: Distributed, Visualized Constraint Solving (abstract)

Improving SAT-based Bounded Model Checking for Existential CTL through Path Reuse (abstract)

A Theory of Satisfiability-Preserving Proofs in SAT Solving (abstract)

Towards Smarter MACE-style Model Finders (abstract)

The Weak Completion Semantics and Equality (abstract)

Experiments in Verification of Linear Model Predictive Control: Automatic Generation and Formal Verification of an Interior Point Method Algorithm (abstract)

Formal verification of the YubiKey and YubiHSM APIs in Maude-NPA (abstract)

A Verified Efficient Implementation of the LLL Basis Reduction Algorithm (abstract)

LTL with Arithmetic and its Applications in Reasoning about Hierarchical Systems (abstract)

Rewriting Environment for Arithmetic Circuit Verification (abstract)

Is Satisfiability of Quantified Bit-Vector Formulas Stable Under Bit-Width Changes? (abstract)

HoTT-Crypt : A Study in Homotopy Type Theory based on Cryptography (abstract)

Commonsense Reasoning for Robotics and Bioscience via Probabilistic Logic and Meta-learning (abstract)

The Involutions-as-Principal Types/Application-as-Unification Analogy (abstract)

Knowledge Compilation meets Uniform Sampling (abstract)

Graphs Path Orderings (abstract)

Why These Automata Types? (abstract)

Lyndon Interpolation holds for the Prenex ⊃ Prenex Fragment of Gödel Logic (abstract)

Matching in the Description Logic FL0 with respect to General TBoxes (abstract)

The Triguarded Fragment of First-order Logic (abstract)