Mission and Vision logo Mission and Vision

Our mission is accessible trustworthy computing. We accomplish it by generating correct-by-construction implementations and tools automatically, from their specifications. One of our unique technologies is K, a semantic framework for design, implementation and formal reasoning.

About Runtime Verification 2020-10-16

About Runtime Verification: PDF | PPTX

About Runtime Verification (1'50")

What is K?

K is a semantic framework for design, implementation and formal reasoning that allows language designers to formally define their language using an intuitive and attractive notation, and generate for free the implementations and the analysis tools for that defined language.

What is K 2020-10-16

What is K?: PDF | PPTX

What is K? (16'30")

Concrete Execution

When instantiating a generic K tool to a particular language semantics, like we do here with the K concrete execution engine which is instantiated with the C semantics, a challenge we face is how to make K and its complexity invisible to the user.

Concrete Execution 2020-10-16

Concrete Execution: PDF | PPTX

Concrete Execution (11'35")

company mission and vision news team careers publications presentations videos faq Embedded Systems Blockhain Advisory Services Smart Contract Verification Protocol Verification Formal Design and Modeling The IELE Virtual Machine Partnerships contact media kit blog