Computer-Aided Program Development Group

Dipl.-Math. Insa Stucke

Research assistant

Christian-Albrechts-Platz 4, R. 713 (CAP 4)
Phone: +49 431 880-7274
Telefax: +49 431 880-7613
ist@informatik.uni-kiel.de

Fields of interest

  • relation algebra
  • graph algorithms
  • software verification
  • automated and interactive theorem provers

Publications

  • Insa Stucke:
    Reasoning about Cardinalities of Relations with Applications Supported by Proof Assistants. RAMiCS 2017 (to appear)
  • P. Brunet, D. Pous, I. Stucke: 
    Cardinalities of Finite Relations in Coq (Rough Diamond). ITP 2016, LNCS 9807 pp. 466-474, Springer 2016.
  • R. Berghammer, N. Danilenko, P. Höfner, I. Stucke: 
    Cardinality of Relations with Applications. Journal of Discrete Mathematics 339, pp. 3089-3115. 2016.
  • R. Berghammer, P. Höfner, I. Stucke: 
    Cardinality of relations and relational approximation algorithms. Journal of Logical and Algebraic Methods in Programming 85, pp. 269-286. 2016.
  • Rudolf Berghammer, Insa Stucke, Michael Winter:
    Investigating and Computing Bipartitions with Algebraic Means. RAMiCS 2015, LNCS 9348, pp. 257-274. Springer 2015
  • Rudolf Berghammer, Peter Höfner, Insa Stucke:
    Tool-Based Verification of a Relational Vertex Coloring Program. RAMiCS 2015, LNCS 9348, pp. 275-292. Springer 2015
  • Rudolf Berghammer, Peter Höfner, Insa Stucke:
    Automated Verification of Relational While-Programs. RAMiCS 2014, LNCS 8248, pp. 309-326. Springer 2014

Teaching

Winter term 2016/2017

  • Übung: Mathematik für Informatiker A
  • Globalübung: Mathematik für Informatiker A
  • Seminar: Mathematische Methoden in der Informatik (Maschinelles Beweisen)

Winter term 2015/2016

  • Übung: Mathematik für Informatiker A
  • Seminar: Mathematische Methoden in der Informatik (Maschinelles Beweisen)

Summer term 2015

  • Seminar: Mathematische Methoden in der Informatik (Maschinelles Beweisen)

Winter term 2014/2015

  • Übung: Mathematik für Informatiker A

Summer term 2014

  • Übung: Programmierpraktikum
  • Übung: Ordnungen und Verbände

Winter term 2013/2014

  • Übung: Mathematik für Informatiker A
  • Seminar: Mathematische Methoden in der Informatik (Relationale Methoden)

Summer term 2013

  • Übung: Programmierpraktikum
  • Übung: Softwareentwicklung für mobile Geräte

Winter term 2012/2013

  • Übung: Mathematik für Informatiker A
  • Übung: Ordnungen und Verbände
  • Seminar: Mathematische Methoden in der Informatik (Relationale Methoden)

Summer term 2012

  • Übung: Programmierpraktikum

Reasoning about Cardinalities of Relations Supported by Proof Assistants

 

Here, you can find the proof scripts for the paper "Reasoning about Cardinalities of Relations Supported by Proof Assistants" submitted at RAMiCS 2017.

Coq proof scripts  (Compiles with Coq 8.5 and the libraries relation-algebra-1.6 and cardinal.)

Isabelle/HOL library  (Compiles with Isabelle2016 and the library Relation-Algebra.)

 

NEW: Isabelle/HOL library  (Compiles with Isabelle2016.1 and the library Relation-Algebra.)