Logical Completeness for Incorrectness Logic

Bringing verification to software development will be a catalyst for the production of more correct systems and the redirection of effort from code analysis to code creation. Current research on program logics for software verification has focused on providing soundness and completeness while still maintaining scalability and

efficiency. However, work remains to address real practical issues with code abstraction and complex system behaviour. Critically,

pushing for more powerful and easy-to-use tools that identify incorrect behaviour in systems is a step in the right direction towards the mainstream adoption of formal methods in industry Software verification