FUTURES EXPO SERIES
Rationative Systems
Key capabilities
> Automated verification of systems models with respect to specifications about knowledge and time
> Counter example game debugging interface
> Automated synthesis of implementations from knowledge based programs
Differentiators
> Broad spectrum of verification algorithms : BDD , bounded model checking , explicit state model checking
> Best of breed system for automated verification of information theoretic properties
Key partnerships
> Pathology labs looking to expand their capabilities in remote testing and access new population groups
> Population health monitoring to enable large-scale analysis of population groups for critical health measures
> Clinical trials to provide greater engagement and diversity by supporting at-home testing and reducing burden on patients
Quality accreditations and awards
> Australia ’ s Economic Accelerator grant 2024-25
unsw . to / mck
Automated verification of the security and correctness of computer software hardware designs
Start-up
Software errors can have catastrophic consequences , particularly in critical domains such as defence , where human life and national security are at stake . They can also adversely affect financial systems , where there is a risk of large financial losses .
MCK is a unique software verification system developed at UNSW that automatically analyses software models with respect to specifications of correctness and security . It automatically identifies errors and provides a guarantee that there are no errors . This capability will help programmers and code auditors to avoid catastrophic software errors by providing assurance of system correctness and security .
MCK can automatically analyse systems , not just with respect to how the system changes over time , but also the information carried by the systems ’ components .
The team is working on initial commercial application to blockchain smart contracts , distributed autonomous systems , and computer hardware security .
44 •