Design and implement your programming language and software analysis tools with mathematical rigor. Formally verify your programs for maximum assurance.


K gives you

  • a framework for defining formal syntax & semantics of programming languages

  • a suite of execution and analysis tools parametric in your programming language

  • a program verifier whose trust base is your programming language formal semantics


Based on cutting edge research, K allows you to define domain-specific or general-purpose programming languages, and then generate powerful, rigorous, and automatic tools for formally analyzing programs in those languages. No resources wasted anymore to design and implement languages and tools in an adhoc way.


Newsletter

Your email is safe with us

Working with us

What interests you?

Your email

Your phone number

Thank you!

We'll respond to your request within 48 hours

Recent publication

IELE: An Intermediate-Level Blockchain Language Designed and Implemented Using Formal Semantics

Theodoros Kasampalis, Dwight Guth, Brandon Moore, Traian Șerbănuță, Virgil Șerbănuță, Daniele Filaretti, Grigore Roșu, and Ralph Johnson

Technical Report http://hdl.handle.net/2142/100320, July 2018

All publications