Polymorphism and separation in hoare type theoryNANEVSKI, Aleksandar; MORRISETT, Greg; BIRKEDAL, Lars et al.ACM SIGPLAN notices. 2006, Vol 41, Num 9, pp 62-73, issn 1523-2867, 12 p.Conference Paper

THE LOGIC OF ALIASINGCARTWRIGHT R; OPPEN D.1981; ACTA INF.; ISSN 0001-5903; DEU; DA. 1981; VOL. 15; NO 4; PP. 365-384; BIBL. 17 REF.Article

From Control Systems to Control Software: INTEGRATING LYAPUNOV-THEORETIC PROOFS WITHIN CODEFERON, Eric.IEEE control systems. 2010, Vol 30, Num 6, pp 50-71, issn 1066-033X, 22 p.Article

A Probabilistic Hoare-style Logic for Game-Based Cryptographic ProofsCORIN, Ricardo; DEN HARTOG, Jerry.Lecture notes in computer science. 2006, pp 252-263, issn 0302-9743, isbn 3-540-35904-4, 12 p.Conference Paper

An algebraic treatment of procedure refinement to support mechanical verificationBACK, Ralph-Johan; PREOTEASA, Viorel.Formal aspects of computing. 2005, Vol 17, Num 1, pp 69-90, issn 0934-5043, 22 p.Article

From process logic to program logicHONDA, Kohei.ACM SIGPLAN notices. 2004, Vol 39, Num 9, pp 163-174, issn 1523-2867, 12 p.Conference Paper

About hoare logics for higher-order storeREUS, Bernhard; STREICHER, Thomas.Lecture notes in computer science. 2005, pp 1337-1348, issn 0302-9743, isbn 3-540-27580-0, 12 p.Conference Paper

Verification conditions are codeGRAVELL, Andrew M.Acta informatica. 2007, Vol 43, Num 6, pp 431-447, issn 0001-5903, 17 p.Article

Modularity and the rule of adaptationPIERIK, Cees; DE DOER, Frank S.Lecture notes in computer science. 2004, pp 394-408, issn 0302-9743, isbn 3-540-22381-9, 15 p.Conference Paper

Some general in completeness results for partial correctness logicsHORTALA-GONZALEZ, M. T; LUCIO-CARRASCO, F; RODRIGUEZ-ARTALEJO, M et al.Information and computation (Print). 1988, Vol 79, Num 1, pp 22-42, issn 0890-5401Article

Hoare logic in the abstractMARTIN, Ursula; MATHIESEN, Erik A; OLIVA, Paulo et al.Lecture notes in computer science. 2006, pp 501-515, issn 0302-9743, isbn 3-540-45458-6, 1Vol, 15 p.Conference Paper

Hoares's logic for nondeterministic regular programs: a nonstandard approachHORTALA-GONZALEZ, M. T; RODRIGUEZ-ARTALEJO, M.Theoretical computer science. 1989, Vol 68, Num 3, pp 277-302, issn 0304-3975Article

Floyd―Hoare Logic for Quantum ProgramsYING, Mingsheng.ACM transactions on programming languages and systems. 2011, Vol 33, Num 6, issn 0164-0925, 19.1-19.49Article

A compositional natural semantics and Hoare logic for low-level languagesSAABAS, Ando; UUSTALU, Tarmo.Theoretical computer science. 2007, Vol 373, Num 3, pp 273-302, issn 0304-3975, 30 p.Article

Automatic workflow verification and generationSHIYONG LU; BERNSTEIN, Arthur; LEWIS, Philip et al.Theoretical computer science. 2006, Vol 353, Num 1-3, pp 71-92, issn 0304-3975, 22 p.Article

Algebras of modal operators and partial correctnessMÖLLER, Bernhard; STRUTH, Georg.Theoretical computer science. 2006, Vol 351, Num 2, pp 221-239, issn 0304-3975, 19 p.Conference Paper

Frame rules from answer types for code pointersTHIELECKE, Hayo.ACM SIGPLAN notices. 2006, Vol 41, Num 1, pp 309-319, issn 1523-2867, 11 p.Conference Paper

Data refinement and algebraic structureKINOSHITA, Y; POWER, J.Acta informatica. 2000, Vol 36, Num 9-10, pp 693-719, issn 0001-5903Article

Deriving proof rules from continuation semanticsAUDEBAUD, P; ZUCCA, E.Formal aspects of computing. 1999, Vol 11, Num 4, pp 426-447, issn 0934-5043Article

Structuring the Verification of Heap-Manipulating ProgramsNANEVSKI, Aleksandar; VAFEIADIS, Viktor; BERDINE, Josh et al.ACM SIGPLAN notices. 2010, Vol 45, Num 1, pp 261-273, issn 1523-2867, 13 p.Conference Paper

ANOTHER INCOMPLETENESS RESULT FOR HOARE'S LOGICBERGSTRA JA; CHMIELINSKA A; TIURYN J et al.1982; INFORMATION AND CONTROL; ISSN 0019-9958; USA; DA. 1982; VOL. 52; NO 2; PP. 159-171; BIBL. 8 REF.Article

Checking for Deadlock, Double-Free and Other Abuses in the Linux Kernel Source CodeBREUER, Peter T; PICKIN, Simon.Lecture notes in computer science. 2006, pp 765-772, issn 0302-9743, isbn 3-540-34379-2, 8 p.Conference Paper

Cyclic Proofs of Program Termination in Separation LogicBROTHERSTON, James; BORNAT, Richard; CALCAGNO, Cristiano et al.ACM SIGPLAN notices. 2008, Vol 43, Num 1, pp 101-112, issn 1523-2867, 12 p.Conference Paper

Modular Verification of Higher-Order Methods with Mandatory Calls Specified by Model ProgramsSHANER, Steve M; LEAVENS, Gary T; NAUMANN, David A et al.ACM SIGPLAN notices. 2007, Vol 42, Num 10, pp 351-367, issn 1523-2867, 17 p.Conference Paper

A proof outline logic for object-oriented programmingPIERIK, Cees; DE BOER, Frank S.Theoretical computer science. 2005, Vol 343, Num 3, pp 413-442, issn 0304-3975, 30 p.Conference Paper