PORTFOLIO

Entalus offers a comprehensive software design methodology for developing and maintaining software systems hand-in-hand with verifiable evidence for the correctness, dependability, and performance claims.
  • Requirements. Capturing and formally analyzing natural language descriptions.
  • Architecture. Compositional design supporting verification, incrementality, and reuse.
  • Autocoding. Correct-by-construction generation of efficient code from interface contracts.
  • Assurance. Generating, curating and maintaining evidence artifacts and assurance cases.

ACTIVITIES

Roadmapping

Identify and analyze high-impact opportunities for implementing early lifecycle design at clients’ organizations

Engineering

Hands-on engineering support in applying early lifecycle design at clients’ organizations and on clients’ products

Customization

Customization and maintenance of sector-specific specification and assurance artifacts

Empowerment

Hands-on coaching and specialized trainings

BOOTSTRAPPING

Entalus bases its  work and offering on a suite of open-source software development tools, which have originally been developed at SRI International’s Computer Science Labs.

Since Entalus is also participating in ongoing research projects, our clients may benefit through their cooperation with Entalus from recent advances in building software we can actually trust.

Vice versa, the experience and the results obtained through Entalus’ focus on solving real-world should also influence and guide research programmes to focussing on the most impactful research questions.

In this way, Entalus is able to create bootstrapping cycles for focused and impactful research and for accelerated implementation in industrial practice through their mutual reinforcement.

archimedean LEvers

PVS

Formal Specification and Verification

SALLY

Symbolic Analysis Laboratory

YICES

Satisfiability Solver modulo Theories

ETB

Evidential Toolbus

ARSENAL

Semantic Parser Generator

OCCAM

Automated Software Winnowing

RADL

Multirate Integration Architecture

PVS2C

Autocoding C from PVS

PCE

Probabilistic Consistency Engine

Scroll to Top