LARA

Guru

People (tentative):

  • Ruzica
  • Philippe
  • Jiewen
  • Damien

Framework

  • Isabelle-based surface syntax
  • HOTPTP
  • SMT-LIB

Counterexamples

  • SUGA axiomatization from my paper with D.Jackson
  • Fagin's theorem, its consequences on spec language design on finite models, finite domain complexity in practice
  • Ahrendt's work
  • completion for finding infinite models, presentation of infinite models
  • using Ehrenfeucht-Feferman games to find models

References:

Interpolants

  • integer linear arithmetic
  • interpolant combination
  • interpolants for modal mu calculus and MSOL

Interactive Proofs

  • programs as formulas, formulas as proofs
  • tactic style proofs
  • Scala as computational logic

Disjunctive Linear Optimization and Answer-Set Programming

General theme: give more than yes/no answers.