The field of deontic logics and concurrent verification is moving towards the development of more efficient and automated reasoning systems. Researchers are exploring new approaches to formalize conditional norms, reasoning about contradictory but non-trivial propositional attitudes, and verifying complex concurrent programs. A key direction is the integration of deontic logics with other formal systems, such as propositional satisfiability problems and separation logic, to enable more expressive and compositional reasoning. Notable papers in this area include:
- A Reduction of Input/Output Logics to SAT, which presents an automation approach for I/O logics using reductions to propositional satisfiability problems.
- Compositional Verification in Concurrent Separation Logic with Permissions Regions, which introduces a compositional verification system for concurrent programs that manipulate regions of shared memory.