Programming from Control Laws

Search results

• 2014

  Refinement-based verification of implementations of Stateflow charts

  Miyazawa, A. H. & Cavalcanti, A. L. C., 2014, In: Formal Aspects of Computing. 26, 2, p. 367-405

  Research output: Contribution to journal › Article › peer-review

• Test-Data Generation for Control Coverage by Proof

  Cavalcanti, A. L. C., King, S., O'Halloran, C. & Woodcock, J. C. P., Jul 2014, In: Formal Aspects of Computing. 26, 4, p. 795-823 29 p.

  Research output: Contribution to journal › Article › peer-review

• 2013

  Simulink timed models for program verification

  Cavalcanti, A. L. C., Mota, A. & Woodcock, J. C. P., 2013, Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. Vol. 8051 LNCS. p. 82-99

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Testing with Inputs and Outputs in CSP

  Cavalcanti, A. L. C. & Hierons, R., 2013, 16th International Conference, FASE 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013. Vol. 7793 LNCS. p. 359-374

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• 2012

  A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams.

  Marriott, C., Zeyda, F. & Cavalcanti, A. L. C., 2012, Abstract State Machines, Alloy, B, VDM, and Z. Vol. 7316. p. 294-307

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Circus Time with Reactive Designs

  Woodcock, J., Wei, K. & Cavalcanti, A. L. C., 2012, Unifying Theories of Programming . Springer, p. 68-87 (Lecture Notes in Computer Science; vol. 7681).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Mechanical reasoning about families of UTP theories

  Zeyda, F. & Cavalcanti, A. L. C., 1 Apr 2012, In: Science of Computer Programming. 77, 4, p. 444-479 36 p.

  Research output: Contribution to journal › Article › peer-review

• Mechanised support for sound refinement tactics

  Zeyda, F., Oliveira, M. & Cavalcanti, A. L. C., 1 Jan 2012, In: Formal Aspects of Computing. 24, 1, p. 127-160 34 p.

  Research output: Contribution to journal › Article › peer-review

• Refinement-oriented models of stateflow charts

  Miyazawa, A. H. & Cavalcanti, A. L. C., 1 Sept 2012, In: Science of Computer Programming. 77, 10-11, p. 1151-1177 27 p.

  Research output: Contribution to journal › Article › peer-review

• 2011

  A tactic language for refinement of state-rich concurrent specifications

  Oliveira, M., Zeyda, F. & Cavalcanti, A., 1 Sept 2011, In: Science of Computer Programming. 76, 9, p. 792-833 42 p.

  Research output: Contribution to journal › Article › peer-review

• From control law diagrams to Ada via Circus

  Cavalcanti, A., Clayton, P. & O’Halloran , C., Jul 2011, In: Formal Aspects of Computing. 23, 4, p. 1-48 48 p.

  Research output: Contribution to journal › Article › peer-review

• Refinement-based verification of sequential implementations of Stateflow charts

  Miyazawa, A. & Cavalcanti, A., 21 Jun 2011, In: Electronic Proceedings in Theoretical Computer Science. p. 65-83

  Research output: Contribution to journal › Article › peer-review

  File

• Testing for refinement in Circus

  Cavalcanti, A. & Gaudel, M.-C., 1 Apr 2011, In: Acta Informatica. 48, 2, p. 97-147 51 p.

  Research output: Contribution to journal › Article › peer-review

• 2010

  Automating Refinement of Circus Programs

  Zeyda, F. & Cavalcanti, A., 2010, p. 274-290.

  Research output: Contribution to conference › Paper › peer-review

• Communication Systems in ClawZ

  Vernon, M., Zeyda, F. & Cavalcanti, A., 2010, p. 334-348.

  Research output: Contribution to conference › Paper › peer-review

• Specification Coverage for Testing in Circus

  Cavalcanti, A. & Gaudel, M.-C., 2010, p. 1-45.

  Research output: Contribution to conference › Paper › peer-review

• Testing Techniques in Software Engineering: Second Pernambuco Summer School on Software Engineering, PSSE 2007

  Borba, P. (Editor), Cavalcanti, A. (Editor), Sampaio, A. (Editor) & Woodcock, J. (Editor), 2010, Springer. (Lecture Notes in Computer Science; vol. 6153)

  Research output: Book/Report › Book

• 2009

  A UTP semantics for Circus

  Oliveira, M., Cavalcanti, A. & Woodcock, J., 1 Feb 2009, In: Formal Aspects of Computing. 21, 1-2, p. 3-32 30 p.

  Research output: Contribution to journal › Article › peer-review

• Mechanical Reasoning about Families of UTP Theories

  Zeyda, F. & Cavalcanti, A., 2 Jul 2009, In: Electronic Notes in Theoretical Computer Science. 240, C, p. 239-257 19 p.

  Research output: Contribution to journal › Article › peer-review

• Mechanised Translation of Control Law Diagrams into Circus

  Zeyda, F. & Cavalcanti, A., 2009, p. 151-166.

  Research output: Contribution to conference › Paper › peer-review

• Mechanised Translation of Control Law Diagrams into Circus

  Zeyda, F. & Cavalcanti, A., 2009, Integrated Formal Methods. Leuschel, M. & Wehrheim, H. (eds.). Springer, Vol. 5423 LNCS. p. 151-166 16 p. (Lecture Notes in Computer Science; vol. 2999).

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• Stateflow Diagrams in Circus

  Cavalcanti, A., 2 Jul 2009, In: Electronic Notes in Theoretical Computer Science. 240, C, p. 23-41 19 p.

  Research output: Contribution to journal › Article › peer-review

• Supporting ArcAngel in ProofPower

  Zeyda, F., Oliveira, M. & Cavalcanti, A., 31 Dec 2009, In: Electronic Notes in Theoretical Computer Science. 259, C, p. 225-243 19 p.

  Research output: Contribution to journal › Article › peer-review

• 2008

  A Note on Traces Refinement and the it onf Relation in the Unifying Theories of Programming

  Cavalcanti, A. & Gaudel, M.-C., 2008, p. 42-61.

  Research output: Contribution to conference › Paper › peer-review

• ArcAngelC: a Refinement Tactic Language for Circus

  Oliveira, M. & Cavalcanti, A., 28 Jun 2008, In: Electronic Notes in Theoretical Computer Science. 214, C, p. 203-229 27 p.

  Research output: Contribution to journal › Article › peer-review

• Encoding it ircus Programs in ProofPowerZ

  Zeyda, F. & Cavalcanti, A., 2008, p. 218-237.

  Research output: Contribution to conference › Paper › peer-review

• Type Checking Circus Specifications

  Xavier, M., Cavalcanti, A. & Sampaio, A., 18 Jan 2008, In: Electronic Notes in Theoretical Computer Science. 195, C, p. 75-93 19 p.

  Research output: Contribution to journal › Article › peer-review

• 2007

  Testing for refinement in CSP

  Cavalcanti, A. & Gaudel, M.-C., 2007, FORMAL METHODS AND SOFTWARE ENGINEERING, PROCEEDINGS. Butler, M., Hinchey, M. & LarrondoPetrie, M. (eds.). BERLIN: Springer, p. 151-170 20 p.

  Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

• 2006

  Angelic Nondeterminism in the Unifying Theories of Programming

  Cavalcanti, A., Woodcock, J. & Dunne, S., Sept 2006, In: Formal Aspects of Computing. 18, 3, p. 288-307 19 p.

  Research output: Contribution to journal › Article › peer-review