List of publications

All pdf files included here are a copy of the author accepted manuscript: post peer-review, but before the publisher has applied their final formatting or copy editing, even if the file itself says otherwise. 

A. Alberto, A. L. C. Cavalcanti, M.-C. Gaudel, and A. Simao. Formal mutation testing for Circus. Information and Software Technology, 81:131--153, 2017. [ bib | DOI | .pdf ]

M. Luckcuck, A. Wellings, and A. L. C. Cavalcanti. Safety-Critical Java: level 2 in practice. Concurrency and Computation: Practice and Experience, 9, 2017. [ bib | DOI ]

S. Foster, B. Thiele, and A. L. C. Cavalcanti J. C. P. Woodcock. Towards a UTP Semantics for Modelica. In J. Bowen and H. Zhu, editors, 6th International Symposium on Unifying Theories of Programming, volume 10134 of Lecture Notes in Computer Science, pages 44--64. Springer, 2017. [ bib | DOI | .pdf ]

P. Ribeiro, A. L. C. Cavalcanti, and J. C. P. Woodcock. A Stepwise Approach to Linking Theories. In J. Bowen and H. Zhu, editors, 6th International Symposium on Unifying Theories of Programming, volume 10134 of Lecture Notes in Computer Science, pages 134--154. Springer, 2017. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, A. Miyazawa, A. Wellings, J. C. P. Woodcock, and S. Zhao. Java in the Safety-Critical Domain. In J. Bowen, Z. Liu, and Z. Zhang, editors, Engineering Trustworthy Software Systems, volume 10215 of Lecture Notes in Computer Science, pages 110--150. Springer, 2017. [ bib | DOI | .pdf ]

A. Miyazawa, P. Ribeiro, W. Li, A. L. C. Cavalcanti, and J. Timmis. Automatic property checking of robotic applications. In The International Conference on Intelligent Robots and Systems, 2017. [ bib ]

P. Ribeiro, A. Miyazawa, W. Li, A. L. C. Cavalcanti, and J. Timmis. Modelling and verification of timed robotic controllers. In N. Polikarpova and S. Schneider, editors, Integrated Formal Methods, pages 18--33. Springer, 2017. [ bib | DOI | .pdf ]

J. Baxter and A. L. C. Cavalcanti. Algebraic compilation of safety-critical java bytecode. In N. Polikarpova and S. Schneider, editors, Integrated Formal Methods, pages 161--176. Springer, 2017. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and A. Simao. Fault-based testing for refinement in CSP. In N. Yevtushenko, A. R. Cavalli, and H. Yenigün, editors, 29th IFIP WG 6.1 International Conference on Testing Software and Systems, volume 10533 of Lecture Notes in Computer Science, pages 21--37. Springer, 2017. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, A. Miyazawa, R. Payne, and J. Woodcock. Sound Simulation and Co-simulation for Robotics, pages 173--194. Springer International Publishing, 2017. [ bib | DOI | .pdf ]

L. Freitas, J. Baxter, A. L. C. Cavalcanti, and A. Wellings. Modelling and verifying a priority scheduler for an SCJ runtime environment. In E. Ábrahám and M. Huisman, editors, Integrated Formal Methods, volume 9681 of Lecture Notes in Computer Science, pages 63--78. Springer, 2016. [ bib | DOI | .pdf ]

M. Luckcuck, A. L. C. Cavalcanti, and A. Wellings. A Formal Model of the Safety-Critical Java Level 2 Paradigm. In E. Ábrahám and M. Huisman, editors, Integrated Formal Methods, volume 9681 of Lecture Notes in Computer Science, pages 226--241. Springer, 2016. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, J. C. P. Woodcock, and N. Amálio. Behavioural Models for FMI Co-simulations. In A. C. A. Sampaio and F. Wang, editors, International Colloquium on Theoretical Aspects of Computing, volume 9965 of Lecture Notes in Computer Science, pages 255--273. Springer, 2016. [ bib | DOI | .pdf ]

N. Amálio, R. Payne, A. L. C. Cavalcanti, and J. C. P. Woodcock. Checking SysML Models for Co-Simulation. In International Conference on Formal Engineering Methods, volume 10009 of Lecture Notes in Computer Science, pages 450--465. Springer, 2016. [ bib | DOI | .pdf ]

M. Conserva Filho, M. V. M. Oliveira, A. C. A. Sampaio, and A. L. C. Cavalcanti. Local Livelock Analysis of Component-Based Models. In International Conference on Formal Engineering Methods, volume 10009 of Lecture Notes in Computer Science, pages 279--295. Springer, 2016. [ bib | DOI | .pdf ]

G. Carvalho, A. L. C. Cavalcanti, and A. C. A. Sampaio. Modelling Timed Reactive Systems from Natural-Language Requirements. Formal Aspects of Computing, 28(5):725--765, 2016. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, R. M. Hierons, S. Nogueira, and A. C. A. Sampaio. A suspension-trace semantics for CSP. In International Symposium on Theoretical Aspects of Software Engineering, pages 3--13, 2016. Invited paper. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and M.-C. Gaudel. Test selection for traces refinement. Theoretical Computer Science, 563(0):1 -- 42, 2015. [ bib | DOI | .pdf ]

F. Zeyda and A. L. C. Cavalcanti. Laws of mission-based programming. Formal Aspects of Computing, pages 1--50, 2015. [ bib | DOI | .pdf ]

A. Miyazawa and A. L. C. Cavalcanti. SCJ-Circus: a refinement-oriented formal notation for Safety-Critical Java. In REFINE Workshop. 2015. [ bib | http ]

G. Carvalho, F. A. Barros, A. Carvalho, A. L. C. Cavalcanti, A. Mota, and A. C. A. Sampaio. NAT2TEST tool: From natural language requirements to test cases based on CSP. In R. Calinescu and B. Rumpe, editors, 13th International Conference Software Engineering and Formal Methods, volume 9276 of Lecture Notes in Computer Science, pages 283 -- 290. Springer, 2015. [ bib | DOI | .pdf ]

L. Lima, A. Miyazawa, A. L. C. Cavalcanti, M. Cornélio, J. Iyoda, A. C. A. Sampaio, R. Hains, A. Larkham, and V. Lewis. An integrated semantics for reasoning about SysML design models using refinement. Software & Systems Modeling, pages 1 -- 28, 2015. [ bib | DOI | .pdf ]

J. Baxter, A. L. C. Cavalcanti, A. J. Wellings, and L. Freitas. Safety-Critical Java Virtual Machine Services. In L. Ziarek, editor, 13th International Workshop on Java Technologies for Real-time and Embedded Systems, pages 7:1--7:10. ACM, 2015. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, W.-L. Huang, J. Peleska, and J. C. P. Woodcock. CSP and Kripke Structures. In M. Leucker, C. Rueda, and F. D. Valencia, editors, Theoretical Aspects of Computing, pages 505--523. Springer, 2015. [ bib | DOI | .pdf ]

A. Miyazawa and A. L. C. Cavalcanti. Refinement strategies for Safety-Critical Java. In M. L. Cornélio, editor, Brazilian Symposium on Formal Methods, Lecture Notes in Computer Science. Springer, 2015. [ bib | DOI | .pdf ]

J. C. P. Woodcock, A. J. Wellings, and A. L. C. Cavalcanti. Mobile CSP. In M. L. Cornélio, editor, Brazilian Symposium on Formal Methods, Lecture Notes in Computer Science. Springer, 2015. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti. Can Java Ever Be Safe? The hiJaC Project Abstract. In M. Butler, S. Conchon, and F. Zaïdi, editors, 17th International Conference on Formal Engineering Methods, volume 9407 of Lecture Notes in Computer Science. Springer, 2015. Invited. [ bib ]

A. Miyazawa and A. L. C. Cavalcanti. Refinement-based verification of implementations of Stateflow charts. Formal Aspects of Computing, 26(2):367--405, 2014. [ bib | DOI | .pdf ]

F. Zeyda, L. Lalkhumsanga, A. L. C. Cavalcanti, and A. Wellings. Circus Models for Safety-Critical Java Programs. The Computer Journal, 57(7):1046--1091, 2014. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and M.-C. Gaudel. Data Flow coverage for Circus-based testing. In Fundamental Approaches to Software Engineering, volume 8441 of Lecture Notes in Computer Science, pages 415--429, 2014. [ bib | DOI | .pdf ]

F. Zeyda, T. L. V. L. Santos, A. L. C. Cavalcanti, and A. C. A. Sampaio. A modular theory of object orientation in higher-order UTP. In Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 627--642. Springer, 2014. [ bib | DOI | .pdf ]

C. Marriott and A. L. C. Cavalcanti. SCJ: Memory-safety checking without annotations. In Formal Methods, volume 8442 of Lecture Notes in Computer Science, pages 465--480. Springer, 2014. [ bib | DOI | .pdf ]

P. Ribeiro and A. L. C. Cavalcanti. Angelicism in the theory of reactive processes. In Unifying Theories of Programming, Lecture Notes in Computer Science. Springer, 2014. [ bib | DOI | .pdf ]

S. Foster, A. Miyazawa, J. C. P. Woodcock, A. L. C. Cavalcanti, J. Fitzgerald, and P. G. Larsen. An approach for managing semantic heterogeneity in Systems of Systems Engineering. In 9th International Conference on Systems of Systems Engineering, IEEE Systems Journal. IEEE, 2014. [ bib | DOI | .pdf ]

J. C. P. Woodcock, A. L. C. Cavalcanti, J. Fitzgerald, S. Foster, and P. G. Larsen. Contracts in CML. In 6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Lecture Notes in Computer Science. Springer, 2014. [ bib | DOI | .pdf ]

R. Hawkins, A. Miyazawa, A. L. C. Cavalcanti, T. Kelly, and J. Rowlands. Assurance Cases for Block-configurable Software. In 33rd International Conference on Computer Safety, Reliability and Security, Lecture Notes in Computer Science. Springer, 2014. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, S. King, C. O'Halloran, and J. C. P. Woodcock. Test-Data Generation for Control Coverage by Proof. Formal Aspects of Computing, 26(4):795--823, 2014. [ bib | DOI | .pdf ]

A. Miyazawa and A. L. C. Cavalcanti. Formal Refinement in SysML. In E. Albert and E. Sekerinski, editors, 11th International Conference on Integrated Formal Methods, Lecture Notes in Computer Science, pages 155--170. Springer, 2014. [ bib | DOI | .pdf ]

P. Ribeiro and A. L. C. Cavalcanti. UTP Designs for Binary Multirelations. In G. Ciobanu and D. Méry, editors, Theoretical Aspects of Computing, volume 8687 of Lecture Notes in Computer Science, pages 388--405. Springer, 2014. [ bib | DOI | .pdf ]

G. Carvalho, A. Carvalho, E. Rocha, A. L. C. Cavalcanti, and A. C. A. Sampaio. A formal model for natural-language timed requirements of reactive systems. In S. Merz and J. Pang, editors, Formal Methods and Software Engineering, volume 8829 of Lecture Notes in Computer Science, pages 43--58. Springer, 2014. [ bib | DOI | .pdf ]

A. L. .C Cavalcanti, A. Wellings, and J. C. P. Woodcock. The Safety-Critical Java memory model formalised. Formal Aspects of Computing, 25(1):37--57, 2013. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and R. M. Hierions. Testing with Inputs and Outputs in CSP. In Fundamental Approaches to Software Engineering, volume 7793 of Lecture Notes in Computer Science, pages 359--374, 2013. [ bib | DOI | .pdf ]

P. Ribeiro and A. L. C. Cavalcanti. Designs with angelic nondeterminism. In 7th International Symposium on Theoretical Aspects of Software Engineering, pages 71--78. IEEE, 2013. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, F. Zeyda, A. Wellings, J. C. P. Woodcock, and K. Wei. Safety-critical Java programs from Circus models. Real-Time Systems, 49(5):614--667, 2013. [ bib | DOI | .pdf ]

M. V. M. Oliveira, A. L. C. Cavalcanti, and J. C. P. Woodcock. Unifying theories in ProofPower-Z. Formal Aspects of Computing, 25(1):133--158, 2013. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, A. Mota, and J. C. P. Woodcock. Simulink timed models for program verification. In Z. Liu, J. C. P. Woodcock, and H. Zhu, editors, Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday, volume 8051 of Lecture Notes in Computer Science, pages 82--99. Springer, 2013. [ bib | DOI | .pdf ]

A. Miyazawa, L. Lima, and A. L. C. Cavalcanti. Formal Models of SysML Blocks. In L. Groves and J. Sun, editors, 15th International Conference on Formal Engineering Methods, volume 8144 of Lecture Notes in Computer Science, pages 249--264. Springer, 2013. [ bib | DOI | .pdf ]

F. Zeyda and A. L. C. Cavalcanti. Refining SCJ Mission Specifications into Parallel Handler Designs. In J. Derrick, E. A. Boiten, and S. Reeves, editors, 16th International Refinement Workshop, volume 115 of EPTCS, pages 52--67, 2013. [ bib | DOI | .pdf ]

F. Zeyda and A. L. C. Cavalcanti. Higher-Order UTP for a Theory of Methods. In B. Wolff, M.-C. Gaudel, and A. Feliachi, editors, Unifying Theories of Programming, volume 7681 of Lecture Notes in Computer Science, pages 204--223. Springer, 2013. [ bib | DOI | .pdf ]

K. Wei, J. C. P. Woodcock, and A. L. C. Cavalcanti. Circus Time with Reactive Designs. In B. Wolff, M.-C. Gaudel, and A. Feliachi, editors, Unifying Theories of Programming, volume 7681 of Lecture Notes in Computer Science. Springer, 2013. [ bib | DOI | .pdf ]

A. J. Wellings, M. Luckcuck, and A. L. C Cavalcanti. Safety-critical Java level 2: motivations, example applications and issues. In F. Siebert and K. Nilsen, editors, The 11th International Workshop on Java Technologies for Real-time and Embedded Systems, pages 48--57. ACM, 2013. [ bib | DOI | .pdf ]

A. J. Wellings, A. Burns, A. L. C. Cavalcanti, and N. K. Singh. Programming Simple Reactive Systems in Ada: Premature Program Termination. Ada Letters, 33(2):75--86, 2013. [ bib | DOI | .pdf ]

F. Zeyda and A. L. C. Cavalcanti. Mechanical Reasoning about Families of UTP Theories. Science of Computer Programming, 77(4):444--479, 2012. [ bib | DOI | .pdf ]

F. Zeyda, M. V. M. Oliveira, and A. L. C. Cavalcanti. Mechanised support for sound refinement tactics. Formal Aspects of Computing, 24(1):127--160, 2012. [ bib | DOI | .pdf ]

C. Marriott, F. Zeyda, and A. L. C. Cavalcanti. A Tool Chain for the Automatic Generation of Circus Specifications of Simulink Diagrams. In J. Derrick, J. Fitzgerald, S. Gnesi, S. Khurshid, M. Leuschel, S. Reeves, and E. Riccobene, editors, Abstract State Machines, Alloy, B, VDM, and Z, volume 7316 of Lecture Notes in Computer Science, pages 294--307. Springer, 2012. [ bib | DOI | .pdf ]

A. Miyazawa and A. L. C. Cavalcanti. Refinement-oriented models of Stateflow charts. Science of Computer Programming, 77(10-11):1151--1177, 2012. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, editor. Science of Computer Programming, volume 77(12). Elsevier, 2012. Special issue. Guest editor. [ bib ]

A. L. C. Cavalcanti and D. Déharbe, editors. Theoretical Computer Science, volume 455. Elsevier, 2012. Special issue. Guest editors. [ bib ]

N. K. Singh, A. J. Wellings, and A. L. C. Cavalcanti. The cardiac pacemaker case study and its implementation in safety-critical Java and Ravenscar Ada. In 10th International Workshop on Java Technologies for Real-time and Embedded Systems, pages 62--71. ACM, 2012. [ bib | DOI | .pdf ]

J. C. P. Woodcock, A. L. C. Cavalcanti, J. Fitzgerald, P. G. Larsen, A. Miyazawa, and S. Perry. Features of CML: a Formal Modelling Language for Systems of Systems. In 7th International Conference on Systems of Systems Engineering, volume 6 of IEEE Systems Journal. IEEE, 2012. [ bib | DOI | .pdf ]

A. Miyazawa and A. L. C. Cavalcanti. Refinement-based verification of sequential implementations of Stateflow charts. In J. Derrick, E. Boiten, and S. Reeves, editors, Refinement Workshop, Electronic Notes in Theoretical Computer Science. Elsevier, 2011. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, A. Wellings, and J. C. P. Woodcock. The Safety-critical Java Memory Model: a formal account. In M. Butler and W. Schulte, editors, Formal Methods, volume 6664 of Lecture Notes in Computer Science, pages 246--261. Springer-Verlag, 2011. [ bib | DOI | .pdf ]

F. Zeyda, A. L. C. Cavalcanti, and A. Wellings. The Safety-critical Java Mission Model: a formal account. In International Conference on Formal Engineering Methods, volume 6991 of Lecture Notes in Computer Science, pages 49--65, 2011. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, A. Wellings, J. C. P. Woodcock, K. Wei, and F. Zeyda. Safety-Critical Java in Circus. In A. P. Ravn, editor, 9th Workshop on Java Technologies for Real-Time and Embedded System, ACM Digital Library. ACM, 2011. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, M.-C. Gaudel, and R. M. Hierons. Conformance Relations for Distributed Testing based on CSP. In B. Wolff and F. Zaidi, editors, IFIP International Conference on Testing Software and Systems, Lecture Notes in Computer Science. Springer-Verlag, 2011. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and M.-C. Gaudel. Testing for Refinement in Circus. Acta Informatica, 48(2):97--147, 2011. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, P. Clayton, and C. O'Halloran. From Control Law Diagrams to Ada via Circus. Formal Aspects of Computing, 23(4):465--512, 2011. [ bib | DOI | .pdf ]

M. V. M. Oliveira, F. Zeyda, and A. L. C. Cavalcanti. A tactic language for refinement of state-rich concurrent specifications. Science of Computer Programming, 76(9):792--833, 2011. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and D. Dams, editors. Formal Aspects of Computing, volume 23(6). Springer, 2011. Special issue. Guest editors. [ bib ]

A. L. C. Cavalcanti and D. Dams, editors. Formal Methods in System Design, volume 37(2-3). Springer, 2011. Special issue. Guest editors. [ bib ]

P. H. M. Borba, A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock, editors. Testing Techniques in Software Engineering, volume 6153 of Lecture Notes in Computer Science. Springer, 2010. [ bib ]

R. F. Paige, J. C. P. Woodcock, P. J. Brooke, and A. L. C. Cavalcanti. Programming phase: Formal methods. In Encyclopedia of Software Engineering, pages 772--785. John Wiley and Sons, Inc., 2010. [ bib ]

M. Vernon, F. Zeyda, and A. L. C. Cavalcanti. Communication Systems in ClawZ. In Abstract State Machines, Alloy, B, and Z, volume 5977 of Lecture Notes in Computer Science, pages 334--348. Springer-Verlag, 2010. [ bib | DOI | .pdf ]

F. Zeyda and A. L. C. Cavalcanti. Automating Refinement of Circus Programs. In Brazilian Symposium on Formal Methods, Lecture Notes in Computer Science. Springer-Verlag, 2010. [ bib | DOI | .pdf ]

A. Duran, A. L. C. Cavalcanti, and A. C. A. Sampaio. An Algebraic Approach to the Design of Compilers for Object-oriented Languages. Formal Aspects of Computing, 22(5):489--535, 2010. [ bib | DOI | .pdf ]

A. Sherif, A. L. C. Cavalcanti, J. He, and A. C. A. Sampaio. A process algebraic framework for specification and validation of real-time systems. Formal Aspects of Computing, 22(2):153--191, 2010. [ bib | DOI | .pdf ]

M. Cornélio, A. L. C. Cavalcanti, and A. C. A. Sampaio. Sound Refactorings. Science of Computer Programming, 75(3):106--133, 2010. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, D. Deharbe, M.-C. Gaudel, and J. C. P. Woodcock, editors. Theoretical Aspects of Computing, volume 6255 of Lecture Notes in Computer Science. Springer-Verlag, 2010. [ bib ]

A. L. C. Cavalcanti and M.-C. Gaudel. A note on traces refinement and the conf relation in the Unifying Theories of Programming. In A. Butterfield, editor, Unifying Theories of Programming, volume 5713 of Lecture Notes in Computer Science. Springer-Verlag, 2010. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and M.-C. Gaudel. Specification Coverage for Testing in Circus. In S. Qin, editor, Unifying Theories of Programming, volume 6445 of Lecture Notes in Computer Science, pages 1--45. Springer-Verlag, 2010. [ bib | DOI | .pdf ]

K. Breitman and A. L. C. Cavalcanti, editors. Formal Methods and Software Engineering, volume 5885 of Lecture Notes in Computer Science. Springer-Verlag, 2009. [ bib ]

A. L. C. Cavalcanti and D. R. Dams, editors. FM 2009: Formal Methods, volume 5850 of Lecture Notes in Computer Science. Springer-Verlag, 2009. [ bib ]

M. V. M. Oliveira, A. L. C. Cavalcanti, and J. C. P. Woodcock. A UTP Semantics for Circus. Formal Aspects of Computing, 21(1-2):3--32, 2009. [ bib | DOI | .pdf ]

F. Zeyda and A. L. C. Cavalcanti. Encoding Circus Programs in ProofPower-Z. In Unifying Theories of Programming, Lecture Notes in Computer Science. Springer-Verlag, 2009. [ bib | DOI | .pdf ]

F. Zeyda and A. L. C. Cavalcanti. Mechanised Translation of Control Law Diagrams into Circus. In M. Leuschel and H. Wehrheim, editors, Integrated Formal Methods, volume 5423 of Lecture Notes in Computer Science, pages 151--166. Springer-Verlag, 2009. [ bib | DOI | .pdf ]

F. Zeyda, M. V. M. Oliveira, and A. L. C. Cavalcanti. Supporting ArcAngel in ProofPower. Electronic Notes in Theoretical Computer Science, 259:225--243, 2009. 14th BCS-FACS Refinement Workshop (REFINE 2009). [ bib | DOI ]

M. V. M. Oliveira and A. L. C. Cavalcanti. ArcAngelC: a Refinement Tactic Language for Circus. Electronic Notes in Theoretical Computer Science, 214C:203--229, 2008. [ bib | DOI | .pdf ]

W. Harwood, A. L. C. Cavalcanti, and J. C. P. Woodcock. A Theory of Pointers for the UTP. In J. S. Fitzgerald, A. E. Haxthausen, and H. Yenigun, editors, Theoretical Aspects of Computing, volume 5160 of Lecture Notes in Computer Science, pages 141--155. Springer-Verlag, 2008. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti. Stateflow diagrams in Circus. In P. Machado, editor, SBMF 2008: Brazilian Symposium on Formal Methods, Electronic Notes in Theoretical Computer Science. Elsevier B. V., 2008. Invited paper. [ bib | DOI | .pdf ]

F. Zeyda and A. L. C. Cavalcanti. Mechanical Reasoning about Families of UTP Theories. In P. Machado, editor, SBMF 2008: Brazilian Symposium on Formal Methods. Elsevier B. V., 2008. Best paper award. [ bib | DOI ]

K. Barkaoui, M. Broy, A. L. C. Cavalcanti, and A. Cerone, editors. Formal Aspects of Computing, volume 20(4-5). Springer, 2008. Special issue. Guest editors. [ bib ]

A. L. C. Cavalcanti and M.-C. Gaudel. Testing for Refinement in CSP. In 9th International Conference on Formal Engineering Methods, volume 4789 of Lecture Notes in Computer Science, pages 151--170. Springer-Verlag, 2007. [ bib | DOI | .pdf ]

L. J. S. Freitas, J. C. P. Woodcock, and A. L. C. Cavalcanti. An Architecture for Circus Tools. In A. C. V. Melo and A. Moreira, editors, Brazilian Symposium on Formal Methods, pages 6--21, 2007. [ bib | .pdf ]

A. L. C. Cavalcanti and P. Clayton. Verification of Control Systems using Circus. In 11th IEEE International Conference on Engineering of Complex Computer Systems, pages 269--278. IEEE Computer Society, 2006. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock, editors. Refinement Techniques in Software Engineering, volume 3167 of Lecture Notes in Computer Science. Springer-Verlag, 2006. [ bib ]

K. Barkaoui, A. L. C. Cavalcanti, and A. Cerone, editors. Theoretical Aspects of Computing, volume 4281 of Lecture Notes in Computer Science. Springer-Verlag, 2006. [ bib ]

A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. Refinement: An Overview. In Refinement Techniques in Software Engineering, volume 3167 of Lecture Notes in Computer Science, pages 1--17. Springer-Verlag, 2006. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and J. C. P. Woodcock. A Tutorial Introduction to CSP in Unifying Theories of Programming. In Refinement Techniques in Software Engineering, volume 3167 of Lecture Notes in Computer Science, pages 220--268. Springer-Verlag, 2006. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, J. C. P. Woodcock, and S. Dunne. Angelic Nondeterminism in the Unifying Theories of Programming. Formal Aspects of Computing, 18(3):288--307, 2006. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, W. Harwood, and J. C. P. Woodcock. Pointers and Records in the Unifying Theories of Programming. In S. Dunne and B. Stoddart, editors, Unifying Theories of Programming, volume 4010 of Lecture Notes in Computer Science, pages 200--216. Springer-Verlag, 2006. [ bib | DOI | .pdf ]

A. F. Freitas and A. L. C. Cavalcanti. Automatic Translation from Circus to Java. In J. Misra, T. Nipkow, and E. Sekerinski, editors, Formal Methods, volume 4085 of Lecture Notes in Computer Science, pages 115--130. Springer-Verlag, 2006. [ bib | DOI | .pdf ]

L. J. S. Freitas, A. L. C. Cavalcanti, and J. C. P. Woodcock. Taking our own medicine: applying the refinement calculus to state-rich refinement model checking. In Z. Liu and J. He, editors, International Conference on Formal Engineering Methods, volume 4260 of Lecture Notes in Computer Science, pages 697--716. Springer-Verlag, 2006. [ bib | DOI | .pdf ]

L. J. S. Freitas, J. C. P. Woodcock, and A. L. C. Cavalcanti. State-rich model checking. Innovations in Systems and Software Engineering, 2(1):49--64, 2006. [ bib | DOI | .pdf ]

M. V. M. Oliveira, A. L. C. Cavalcanti, and J. C. P. Woodcock. Unifying Theories in ProofPower-Z. In S. Dunne and B. Stoddart, editors, Unifying Theories of Programming, volume 4010 of Lecture Notes in Computer Science, pages 123--140. Springer-Verlag, 2006. [ bib | DOI | .pdf ]

M. V. M. Oliveira, A. L. C. Cavalcanti, and J. C. P. Woodcock. A denotational semantics for Circus. In B. Aichernig and J. Derrick, editors, REFINE'2006, Eletronic Notes in Theoretical Computer Science. Elsevier, 2006. [ bib | DOI ]

T. L. V. L. Santos, A. L. C. Cavalcanti, and A. C. A. Sampaio. Object Orientation in the UTP. In S. Dunne and B. Stoddart, editors, Unifying Theories of Programming, volume 4010 of Lecture Notes in Computer Science, pages 18--37. Springer-Verlag, 2006. [ bib | DOI | .pdf ]

S. Schneider, A. L. C. Cavalcanti, H. Treharne, and J. C. P. Woodcock. A Layered Behavioural Model of Platelets. In 11th IEEE International Conference on Engineering of Complex Computer Systems, pages 98--106. IEEE Computer Society, 2006. [ bib | DOI | .pdf ]

M. A. Xavier, A. L. C. Cavalcanti, and A. C. A. Sampaio. Type Checking Circus Specifications. In A. M. Moreira and L. Ribeiro, editors, Brazilian Symposium on Formal Methods, pages 105--120, 2006. [ bib | DOI ]

A. L. C. Cavalcanti, P. Clayton, and C. O'Halloran. Control Law Diagrams in Circus. In J. Fitzgerald, I. J. Hayes, and A. Tarlecki, editors, FM 2005: Formal Methods, volume 3582 of Lecture Notes in Computer Science, pages 253--268. Springer-Verlag, 2005. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. Unifying Classes and Processes. Software and System Modelling, 4(3):277--296, 2005. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and J. C. P. Woodcock. Angelic Nondeterminism and Unifying Theories of Programming . In J. Derrick and E. Boiten, editors, REFINE 2005, volume 137 of Eletronic Notes in Theoretical Computer Science. Elsevier, 2005. [ bib | DOI ]

M. V. M. Oliveira, A. L. C. Cavalcanti, and J. C. P. Woodcock. Formal development of industrial-scale systems. Innovations in Systems and Software Engineering, 1(2):126--147, 2005. [ bib | DOI | .pdf ]

A. Sherif, J. He, A. L. C. Cavalcanti, and A. C. A. Sampaio. A Framework for Specification and Validation of Real-Time Systems Using Circus Actions. In Z. Liu and K. Araki, editors, International Colloquium on Theoretical Aspects of Computing, volume 3407 of Lecture Notes in Computer Science, pages 478--493. Springer-Verlag, 2005. [ bib | DOI ]

J. C. P. Woodcock, A. L. C. Cavalcanti, and L. Freitas. Operational Semantics for Model-Checking Circus. In J. Fitzgerald, I. J. Hayes, and A. Tarlecki, editors, Formal Methods, volume 3582 of Lecture Notes in Computer Science, pages 237--252. Springer-Verlag, 2005. [ bib | DOI | .pdf ]

M. A. Xavier and A. L. C. Cavalcanti. Mechanised Refinement of Procedures. In Brazilian Symposium on Formal Methods, pages 47--62, 2005. [ bib | DOI ]

M. V. M. Oliveira and A. L. C. Cavalcanti. From Circus to JCSP. In J. Davies et al., editor, International Conference on Formal Engineering Methods, volume 3308 of Lecture Notes in Computer Science, pages 320--340. Springer-Verlag, November 2004. [ bib | DOI | .pdf ]

M. V. M. Oliveira, M. A. Xavier, and A. L. C. Cavalcanti. Refine and Gabriel: Support for Refinement and Tactics. In J. R. Cuellar and Z. Liu, editors, IEEE International Conference on Software Engineering and Formal Methods, pages 310--319. IEEE Computer Society Press, September 2004. [ bib | DOI | .pdf ]

M. V. M. Oliveira, A. L. C. Cavalcanti, and J. C. P. Woodcock. Refining Industrial Scale Systems in Circus. In I. East, J. Martin, P. Welch, D. Duce, and M. Green, editors, Communicating Process Architectures, volume 62 of Concurrent Systems Engineering Series, pages 281--309. IOS Press, September 2004. [ bib | .pdf ]

P. H. M. Borba, A. C. A. Sampaio, A. L. C. Cavalcanti, and M. L. Cornélio. Algebraic Reasoning for Object-Oriented Programming. Science of Computer Programming, 52:53--100, 2004. [ bib | DOI | .pdf ]

M. A. Cornélio, A. L. C. Cavalcanti, and A. C. A.Sampaio. Refactoring Towards a Layered Architecture. In Brazilian Symposium on Formal Methods, volume 95 of Electronic Notes in Theoretical Computer Science, pages 199--216. Elsevier, 2004. [ bib | DOI ]

A. L. C. Cavalcanti and P. Machado, editors. WMF 2003: 6th Brazilian Workshop on Formal Methods, volume 95 of Electronic Notes in Theoretical Computer Science. Elsevier, 2004. [ bib ]

J. C. P. Woodcock and A. L. C. Cavalcanti. A Tutorial Introduction to Designs in Unifying Theories of Programming. In E. A. Boiten, J. Derrick, and G. Smith, editors, IFM 2004: Integrated Formal Methods, volume 2999 of Lecture Notes in Computer Science, pages 40--66. Springer-Verlag, 2004. Invited tutorial. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. A Refinement Strategy for Circus. Formal Aspects of Computing, 15(2 - 3):146--181, 2003. [ bib | DOI | .pdf ]

A. L. C. Cavalcanti and J. C. P. Woodcock. Predicate Transformers in the Semantics of Circus. IEE Proceedings Software, 150(1):85--94, 2003. [ bib | DOI | .pdf ]

A. A. Duran, A. L. C. Cavalcanti, and A. C. A. Sampaio. A Strategy for Compiling Classes, Inheritance, and Dynamic Binding. In K. Araki, S. Gnesi, and D. Mandrioli, editors, Formal Methods, volume 2805 of Lecture Notes in Computer Science, pages 301--320. Springer-Verlag, 2003. [ bib | DOI | .pdf ]

A. F. Freitas, C. M. P. Nascimento, and A. L. C. Cavalcanti. A Refinement Tool for Z. In J. S. Dong and J. C. P. Woodcock, editors, International Conference on Formal Engineering Methods, volume 2885 of Lecture Notes in Computer Science, pages 396--415. Springer-Verlag, 2003. [ bib | DOI ]

M. V. M. Oliveira, A. L. C. Cavalcanti, and J. C. P. Woodcock. ArcAngel: A Tactic Language for Refinement. Formal Aspects of Computing, 15(1):28--47, 2003. [ bib | DOI | .pdf ]

M. L. Cornélio, A. L. C. Cavalcanti, and A. C. A. Sampaio. Refactoring by Transformation. In J. Derrick, E. Boiten, J. C. P. Woodcock, and J. Wright, editors, REFINE'2002, volume 70 of Eletronic Notes in Theoretical Computer Science. Elsevier, 2002. Invited paper. [ bib ]

A. L. C. Cavalcanti and D. A. Naumann. On a Specification-oriented Model for Object-orientation. In 6th Brazilian Symposium on Programming Languages, pages 114--127, 2002. [ bib ]

A. L. C. Cavalcanti and D. A. Naumann. Forward simulation for data refinement of classes. In L. Eriksson and P. A. Lindsay, editors, FME 2002: Formal Methods --- Getting IT Right, volume 2391 of Lecture Notes in Computer Science, pages 471--490. Springer-Verlag, 2002. [ bib ]

A. L. C. Cavalcanti and A. C. A. Sampaio. From CSP-OZ to Java with Processes. In Proceedings of the Workshop on Formal Methods for Parallel Programming, held in conjunction with the International Parallel and Distributed Processing Symposium. IEEE CS Press, 2002. Contained in IPDPS collects proceedings CD-ROM. Abstract appears in IPDPS Proceedings. [ bib ]

A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. Refinement of Actions in Circus. In J. Derrick, E. Boiten, J. C. P. Woodcock, and J. Wright, editors, Proceedings of REFINE'2002, volume 70 of Eletronic Notes in Theoretical Computer Science. Elsevier, 2002. [ bib ]

A. L. C. Cavalcanti and J. C. P. Woodcock. A Weakest Precondition Semantics for Circus. In Communicating Processing Architectures. IOS Press, 2002. [ bib ]

A. A. Duran, A. C. A. Sampaio, and A. L. C. Cavalcanti. Refinement Algebra for Fomal Bytecode Generation. In C. George and H. Miao, editors, International Conference on Formal Engineering Methods, volume 2495 of Lecture Notes in Computer Science, pages 347--358. Springer-Verlag, 2002. [ bib | DOI | .pdf ]

L. J. S. Freitas, A. C. A. Sampaio, and A. L. .C. Cavalcanti. JACK: A Framework for Process Algebra Implementation in Java. In 16th Brazilian Symposium on Software Engineering, pages 98--113, 2002. [ bib ]

B. O. Lira, A. L. C. Cavalcanti, and A C. A. Sampaio. Automation of a Normal Form Reduction Strategy for Object-oriented Programming. In 5th Brazilian Workshop on Formal Methods, pages 193--208, 2002. [ bib ]

A. Sherif, A. L. C. Cavalcanti, and H. Moura. An Action Semantics for Timed CSPm. In 6th Brazilian Symposium on Programming Languages, pages 100--113, 2002. [ bib ]

A. Sherif, A. L. C. Cavalcanti, and H. Moura. Using Abaco to animate a real-time specification language. In Action Semantics Workshop - Federated Logic Conference, BRICS Notes Series, 2002. [ bib ]

A. C. A. Sampaio, J. C. P. Woodcock, and A. L. C. Cavalcanti. Refinement in Circus. In L. Eriksson and P. A. Lindsay, editors, FME 2002: Formal Methods-Getting IT Right, volume 2391 of Lecture Notes in Computer Science, pages 451--470. Springer-Verlag, 2002. [ bib | DOI | .pdf ]

J. C. P. Woodcock and A. L. C. Cavalcanti. The Semantics of Circus. In D. Bert, J. P. Bowen, M. C. Henson, and K. Robinson, editors, Formal Specification and Development in Z and B, volume 2272 of Lecture Notes in Computer Science, pages 184--203. Springer-Verlag, 2002. [ bib | DOI | .pdf ]

J. C. P. Woodcock and A. L. C. Cavalcanti. A Concurrent Language for Refinement. In A. Butterfield and C. Pahl, editors, IWFM'01: 5th Irish Workshop in Formal Methods, BCS Electronic Workshops in Computing, Dublin, Ireland, July 2001. [ bib ]

A. L. C. Cavalcanti and D. A. Naumann. Class Refinement for Sequential Java. In ECOOP 2001 Workshop on Formal Techniques for Java Programs, 2001. [ bib ]

A. Duran, A. C. A. Sampaio, and A. L. C. Cavalcanti. Formal Bytecode Generation for a ROOL Virtual Machine. In 4th Brazilian Workshop on Formal Methods, 2001. [ bib ]

L. Freitas, A. L. C. Cavalcanti, and H. Moura. Animating CSP(M) Using Action Semantics. In 4th Brazilian Workshop on Formal Methods, 2001. [ bib ]

J. C. P. Woodcock and A. L. C. Cavalcanti. The steam boiler in a unified theory of Z and CSP. In 8th Asia-Pacific Software Engineering Conference (APSEC 2001). IEEE Press, 2001. [ bib ]

A. L. C. Cavalcanti and D. A. Naumann. A Weakest Precondition Semantics for Refinement of Object-oriented Programs. IEEE Transactions on Software Engineering, 26(8):713--728, 2000. [ bib ]

A. L. C. Cavalcanti and D. A. Naumann. Simulation and Class Refinement for Java. In S. Drossopoulou, S. Eisenbach, B. Jacobs, G. T. Leavens, P. Müller, and A. Poetzsch-Heffter, editors, ECOOP 2000 Workshop on Formal Techniques for Java Programs. Technical Report 269, Fernuniversität Hagen, 2000. Available from http://www.informatik.fernuni-hagen.de/pi5/publications.html. [ bib ]

L. C. S. Meneses, S. Soares, J. B. Meneses, H. Moura, and A. L. C. Cavalcanti. A Framework for Defining Object-oriented Languages Using Action Semantics. In 4th Brazilian Simposium on Programming Languages, pages 172--185, 2000. [ bib ]

M. V. M. Oliveira and A. L. C. Cavalcanti. Tactics of Refinement. In 14th Brazilian Symposium on Software Engineering, pages 117--132, 2000. [ bib ]

A. L. C. Cavalcanti and D. A. Naumann. A Weakest Precondition Semantics for an Object-oriented Language of Refinement. In J. M. Wing, J. C. P. Woodcock, and J. Davies, editors, FM'99: World Congress on Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1439--1459. Springer-Verlag, 1999. [ bib ]

S. L. Coutinho, T. P. C. Reis, and A. L. C. Cavalcanti. A Tool for Teaching Refinement. In 13th Brazilian Symposium on Software Engineering, pages 61--64, 1999. Tool Session. In Portuguese. [ bib ]

A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. An Inconsistency in Procedures, Parameters, and Substitution the Refinement Calculus. Science of Computer Programming, 33(1):87 -- 96, 1999. [ bib ]

A. L. C. Cavalcanti and J. C. P. Woodcock. ZRC---A Refinement Calculus for Z. Formal Aspects of Computing, 10(3):267---289, 1999. [ bib ]

G. Ramalho, F. Barros, S. Cavalcante, and A. L. C. Cavalcanti et. al. Cyber Rally: An Experience of Democratic Use of the Internet. In H. Bullinger and J. Ziegler, editors, Human-Computer Interaction: Communication, Cooperation, and Application Design, volume 22, pages 402--406. Lawrence Erlbaum Associates, 1999. [ bib ]

A. L. C. Cavalcanti, A. C. A. Sampaio, and J. C. P. Woodcock. Procedures and Recursion in the Refinement Calculus. Journal of the Brazilian Computer Society, 5(1):1--15, 1998. [ bib ]

A. L. C. Cavalcanti and J. C. P. Woodcock. A Weakest Precondition Semantics for Z. The Computer Journal, 41(1):1 -- 15, 1998. [ bib ]

A. L. C. Cavalcanti. A Refinement Calculus for Z. PhD thesis, Oxford University Computing Laboratory, Oxford - UK, 1997. Technical Monograph TM-PRG-123, ISBN 00902928-97-X. [ bib ]

S. R. L. Meira, A. L. C. Cavalcanti, and C. S. Santos. The Unix Filing System: A MooZ Specification. In K. Lano and H. Haughton, editors, Object Oriented Specification Case Studies, chapter 4, pages 80--109. Prentice-Hall, 1994. [ bib ]

S. R. L. Meira and A. L. C. Cavalcanti. MooZ Case Studies. In R. Barden, S. Stepney, and D. Cooper, editors, Object Orientation in Z, chapter 5, pages 37--58. Springer-Verlag, 1992. [ bib ]

S. R. L. Meira and A. L. C. Cavalcanti. Modular Object-Oriented Z Specifications. In J. Nicholls, editor, Z User Workshop, Workshops in Computing, pages 173--192, Oxford - UK, 1990. Springer-Verlag. [ bib ]

A. L. C. Cavalcanti and S. R. L. Meira. Denotational Models of Software Systems. In 9th Conference of the Brazilian Computer Society, pages 187--204, 1989. In Portuguese. [ bib ]

J. Kelner, A. L. C. Cavalcanti, and A. Pardo. LindA: Uma Linguagem para Autoria Automática de Hipertexto. In 3rd Brazilian Symposium on Software Engineering, pages 124--136, 1989. In Portuguese. [ bib ]

R. Sanches, S. Sette, A. L. C. Cavalcanti, D. Florissi, P. Soares, and T. Melo. A Language for a Relational Database Management System. In 2nd Brazilian Symposium on Databases, 1987. In Portuguese. [ bib ]

A. L. C. Cavalcanti, D. Florissi, P. Soares, and T. Melo. Implementation of a Relational Language for Microcomputers. In 7th Conference of the Brazilian Computer Society, pages 441--451, 1987. In Portuguese. [ bib ]


This file was generated by bibtex2html 1.98.