The research behind
the assurance.
The research-lab framing of Giolit Labs — the formal methods, platforms, publications, and developer tooling that underpin our verification, synthesis, and integration work. This is the audience for academic, regulatory, and R&D partners rather than hospital procurement.
Research Areas
Methods we advance
The formal-methods foundations upon which our verification, synthesis, and assurance work is built.
Research Platforms
The engines we build
The underlying platforms behind our tools — the engines that power industrial-scale verification, analysis, synthesis, testing, and integration workflows.
Software Verification Platform
Automated verification of software systems against formal specifications and correctness requirements.
Controller Verification Platform
Analysis and verification of control logic under diverse operational conditions.
Neural Network Assurance Platform
Formal analysis of safety, robustness, and behavioral properties of machine learning systems.
Automated Testing Platform
Intelligent generation and execution of test suites for software validation.
Verified Software Generation Platform
Synthesis of software components from formal specifications with correctness guarantees.
Automated Software Integration Platform
Integration of heterogeneous software components while preserving behavioral consistency and system-level correctness.
Publications
Disseminating advances
Our publications disseminate advances across the following topic areas, in a range of publication formats.
Topic Areas
Publication Types
- Peer-Reviewed Journal Articles
- Conference Papers
- Technical Reports
- White Papers
- Case Studies
- Technology Demonstrations
- Tool Documentation
Publication listings will be added here as they become available — sourced from MDX in-repo or an external CMS.
Developers — Natural-Language to Executable Systems
From language to executable
Next-generation technologies that bridge natural-language specifications, formal models, and executable systems — enabling automatic transformation of high-level requirements into formally analyzable models and executable software artifacts while maintaining correctness and traceability throughout the development lifecycle.
Natural Language → Transition Systems
Transformation of natural-language requirements into formal transition-system representations.
Visualization of Transition Systems
Interactive visualization and exploration of formal behavioral models.
Generation of Programs from Transition Systems
Automatic generation of executable implementations from formal models.
Simulation of Generated Programs
Behavioral analysis and validation of generated software artifacts through simulation.
These technologies support traceable engineering workflows that connect requirements, formal specifications, implementation artifacts, and verification evidence.
Research Collaboration & Technology Transfer
Engage with us
We actively engage with the following organizations through collaborative research, technology transfer, consulting, training, and joint innovation initiatives.
Engagement Types