"D-Case in Agda" Verification Tool (D-Case/Agda)

"D-Case in Agda" Verification Tool (D-Case/Agda) is a system developed at AIST, Japan, which uses Agda for construction and verification of visually structured arguments in D-Cases. A D-Case is a kind of an assurance case for dependability, whose concept is being developed in the project DEOS[^The research is funded by Dependable Embedded Operating Systems for practical use (DEOS) research area in Core Research for Evolutional Science and Technology (CREST) programme of Japan Science and Techonology Agency (JST).^].

D-Case/Agda provides a two-way translation between Agda and D-Case Editor, a graphical editor for D-Case structured arguments. A user can switch back and forth between the two for construction / checking based on formal meaning of a D-Casse and its visual manipulation.

For more information and download instructions, please visit the download page "D-Case in Agda" Verification Tool (D-Case/Agda).