RHLE: Modular Deductive Verification of Relational $$\forall \exists $$ Properties
Robert Dickerson, Qianchuan Ye, Michael K. Zhang, Benjamin Delaware
Topics & Concepts
Computer scienceProgramming languageModular designSet (abstract data type)Relational calculusRelational databaseTheoretical computer scienceHoare logicRefinement calculusExistential quantificationImplementationRelational modelCorrectnessData miningDiscrete mathematicsMathematicsFormal Methods in VerificationSecurity and Verification in ComputingLogic, programming, and type systems