@inproceedings{CFSM87,
author = {R.~Sanches and S.~Sette and A.~L.~C.~Cavalcanti and D.~Florissi and P.~Soares and T.~Melo},
title = {{A Language for a Relational Database Management System}},
booktitle = {{2nd Brazilian Symposium on Databases}},
year = {1987},
note = {In Portuguese.},
owner = {alcc}
}
@inproceedings{SSCFSM87,
author = {A.~L.~C.~Cavalcanti and D.~Florissi and P.~Soares and T.~Melo},
title = {{Implementation of a Relational Language for Microcomputers}},
booktitle = {{7th Conference of the Brazilian Computer Society}},
year = {1987},
pages = {441-451},
note = {In Portuguese.}
}
@inproceedings{CM89,
author = {A.~L.~C.~Cavalcanti and S.~R.~L.~Meira},
title = {{Denotational Models of Software Systems}},
booktitle = {{9th Conference of the Brazilian Computer Society}},
year = {1989},
pages = {187-204},
note = {In Portuguese.}
}
@inproceedings{KCP89,
author = {J.~Kelner and A.~L.~C.~Cavalcanti and A.~Pardo},
title = {{LindA: Uma Linguagem para Autoria Autom\'atica de Hipertexto}},
booktitle = {{3rd Brazilian Symposium on Software Engineering}},
year = {1989},
pages = {124-136},
note = {In Portuguese.}
}
@inproceedings{MC90,
author = {S.~R.~L.~Meira and A.~L.~C.~Cavalcanti},
title = {{Modular Object-Oriented Z Specifications}},
booktitle = {Z User Workshop},
year = {1990},
editor = {J.~Nicholls},
series = {Workshops in Computing},
pages = {173-192},
address = {Oxford - UK},
publisher = {Springer-Verlag}
}
@incollection{MC92,
author = {S.~R.~L.~Meira and A.~L.~C.~ Cavalcanti},
title = {{MooZ Case Studies}},
booktitle = {{Object Orientation in Z}},
publisher = {Springer-Verlag},
year = {1992},
editor = {R.~Barden and S.~Stepney and D.~Cooper},
chapter = {5},
pages = {37-58},
institution = {ZIP/Logica Cambridge Limited}
}
@incollection{MCS94,
author = {S.~R.~L.~Meira and A.~L.~C.~Cavalcanti and C.~S.~Santos},
title = {{The Unix Filing System: A MooZ Specification}},
booktitle = {{Object Oriented Specification Case Studies}},
publisher = {Prentice-Hall},
year = {1994},
editor = {K.~Lano and H.~Haughton},
chapter = {4},
pages = {80-109}
}
@phdthesis{Cav97,
author = {A.~L.~C.~Cavalcanti},
title = {{A Refinement Calculus for Z}},
school = {Oxford University Computing Laboratory},
year = {1997},
address = {Oxford - UK},
note = {Technical Monograph TM-PRG-123, ISBN 00902928-97-X.},
institution = {Oxford University Computing Laboratory},
number = {TM-PRG-101}
}
@article{CSW98,
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
title = {{Procedures and Recursion in the Refinement Calculus}},
journal = {{Journal of the Brazilian Computer Society}},
year = {1998},
volume = {5},
pages = {1-15},
number = {1}
}
@article{CW98,
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{A Weakest Precondition Semantics for Z}},
journal = {The Computer Journal},
year = {1998},
volume = {41},
pages = {1 - 15},
number = {1}
}
@inproceedings{CN99,
author = {A.~L.~C.~Cavalcanti and D.~A.~Naumann},
title = {{A Weakest Precondition Semantics for an Object-oriented Language of Refinement}},
booktitle = {FM'99: World Congress on Formal Methods},
year = {1999},
editor = {J.~M.~Wing and J.~C.~P.~Woodcock and J.~Davies},
volume = {1709},
series = {Lecture Notes in Computer Science},
pages = {1439-1459},
publisher = {Springer-Verlag}
}
@inproceedings{CRC99,
author = {S.~L.~Coutinho and T.~P.~C.~Reis and A.~L.~C.~Cavalcanti},
title = {{A Tool for Teaching Refinement}},
booktitle = {{13th Brazilian Symposium on Software Engineering}},
year = {1999},
pages = {61-64},
note = {Tool Session. In Portuguese.}
}
@article{CSW99,
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
title = {{An Inconsistency in Procedures, Parameters, and Substitution the Refinement Calculus}},
journal = {{Science of Computer Programming}},
year = {1999},
volume = {33},
pages = {87 - 96},
number = {1}
}
@article{CW99,
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{ZRC - A Refinement Calculus for Z}},
journal = {Formal Aspects of Computing},
year = {1999},
volume = {10},
pages = {267-289},
number = {3}
}
@inproceedings{RBCC99,
author = {G.~Ramalho and F.~Barros and S.~Cavalcante and A.~L.~C.~Cavalcanti et. al.},
title = {{Cyber Rally:~An Experience of Democratic Use of the Internet}},
booktitle = {{Human-Computer Interaction:~Communication, Cooperation, and Application Design}},
year = {1999},
editor = {H.~Bullinger and J.~Ziegler},
volume = {22},
pages = {402-406},
publisher = {Lawrence Erlbaum Associates}
}
@article{CN00,
author = {A.~L.~C.~Cavalcanti and D.~A.~Naumann},
title = {{A Weakest Precondition Semantics for Refinement of Object-oriented Programs}},
journal = {IEEE Transactions on Software Engineering},
year = {2000},
volume = {26},
pages = {713-728},
number = {8}
}
@inproceedings{CN00b,
author = {A.~L.~C.~Cavalcanti and D.~A.~Naumann},
title = {{Simulation and Class Refinement for Java}},
booktitle = {{ECOOP 2000 Workshop on Formal Techniques for Java Programs}},
year = {2000},
editor = {S.~Drossopoulou and S.~Eisenbach and B.~Jacobs and G.~T.~Leavens and P.~M{\"u}ller and A.~Poetzsch-Heffter},
organization = {{Technical Report~269, Fernuniversit{\"at} Hagen}},
note = {Available from \verb+www.informatik.fernuni-hagen.de/pi5/publications.html+}
}
@inproceedings{MSMMC00,
author = {L.~C.~S.~Meneses and S.~Soares and J.~B.~Meneses and H.~Moura and A.~L.~C.~Cavalcanti},
title = {{A Framework for Defining Object-oriented Languages Using Action Semantics}},
booktitle = {{4th Brazilian Simposium on Programming Languages}},
year = {2000},
pages = {172-185}
}
@inproceedings{OC00,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti},
title = {{Tactics of Refinement}},
booktitle = {{14th Brazilian Symposium on Software Engineering}},
year = {2000},
pages = {117-132}
}
@inproceedings{CN01,
author = {A.~L.~C.~Cavalcanti and D.~A.~Naumann},
title = {{Class Refinement for Sequential Java}},
booktitle = {{ECOOP 2001 Workshop on Formal Techniques for Java Programs}},
year = {2001}
}
@inproceedings{DSC01,
author = {A.~Duran and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti},
title = {{Formal Bytecode Generation for a ROOL Virtual Machine}},
booktitle = {4th Brazilian Workshop on Formal Methods},
year = {2001}
}
@inproceedings{FCM01,
author = {L.~Freitas and A.~L.~C.~Cavalcanti and H.~Moura},
title = {{Animating CSP(M) Using Action Semantics}},
booktitle = {{4th Brazilian Workshop on Formal Methods}},
year = {2001}
}
@inproceedings{WC01,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
title = {{A Concurrent Language for Refinement}},
booktitle = {{IWFM'01:~5th Irish Workshop in Formal Methods} },
year = {2001},
editor = {A.~Butterfield and C.~Pahl},
series = {BCS Electronic Workshops in Computing},
address = {Dublin, Ireland},
month = {July}
}
@inproceedings{WC01b,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
title = {{The steam boiler in a unified theory of Z and CSP}},
booktitle = {{8th Asia-Pacific Software Engineering Conference (APSEC 2001)}},
year = {2001},
publisher = {IEEE Press}
}
@inproceedings{CCS02,
author = {M.~L.~Corn\'elio and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{Refactoring by Transformation}},
booktitle = {{REFINE'2002}},
year = {2002},
editor = {J.~Derrick and E.~Boiten and J.~C.~P.~Woodcock and J.~Wright},
volume = {70},
series = {Eletronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
note = {Invited paper.}
}
@inproceedings{CN02,
author = {A.~L.~C.~Cavalcanti and D.~A.~ Naumann},
title = {{On a Specification-oriented Model for Object-orientation}},
booktitle = {{6th Brazilian Symposium on Programming Languages}},
year = {2002},
pages = {114-127}
}
@inproceedings{CN02b,
author = {A.~L.~C.~Cavalcanti and D.~A.~Naumann},
title = {{Forward simulation for data refinement of classes}},
booktitle = {{FME 2002: Formal Methods - Getting IT Right}},
year = {2002},
editor = {L.~Eriksson and P.~A.~Lindsay},
volume = {2391},
series = {Lecture Notes in Computer Science},
pages = {471-490},
publisher = {Springer-Verlag}
}
@inproceedings{CS02,
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{From CSP-OZ to Java with Processes}},
booktitle = {{Proceedings of the Workshop on Formal Methods for Parallel Programming, held in conjunction with the International Parallel and Distributed Processing Symposium}},
year = {2002},
publisher = {IEEE CS Press},
note = {Contained in IPDPS collects proceedings CD-ROM. Abstract appears in IPDPS Proceedings.}
}
@inproceedings{CSW02,
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
title = {{Refinement of Actions in \textsf{\emph{Circus}}}},
booktitle = {Proceedings of {REFINE'2002}},
year = {2002},
editor = {J.~Derrick and E.~Boiten and J.~C.~P.~Woodcock and J.~Wright},
volume = {70},
series = {Eletronic Notes in Theoretical Computer Science},
publisher = {Elsevier}
}
@inproceedings{CW02,
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{A Weakest Precondition Semantics for \textsf{\emph{Circus}}}},
booktitle = {{Communicating Processing Architectures}},
year = {2002},
publisher = {IOS Press}
}
@inproceedings{DSC02,
author = {A.~A.~Duran and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti},
title = {{Refinement Algebra for Fomal Bytecode Generation}},
booktitle = {International Conference on Formal Engineering Methods},
year = {2002},
editor = {C.~George and H.~Miao},
volume = {2495},
series = {Lecture Notes in Computer Science},
pages = {347-358},
publisher = {Springer-Verlag},
doi = {10.1007/3-540-36103-0_36},
url = {papers/DSC02.pdf}
}
@inproceedings{FSC02,
author = {L.~J.~S.~Freitas and A.~C.~A.~Sampaio and A.~L.~.C.~Cavalcanti},
title = {{JACK: A Framework for Process Algebra Implementation in Java}},
booktitle = {{16th Brazilian Symposium on Software Engineering}},
year = {2002},
pages = {98-113}
}
@inproceedings{LCS02,
author = {B.~O.~Lira and A.~L.~C.~Cavalcanti and A~C.~A.~Sampaio},
title = {{Automation of a Normal Form Reduction Strategy for Object-oriented Programming}},
booktitle = {5th Brazilian Workshop on Formal Methods},
year = {2002},
pages = {193-208}
}
@inproceedings{SCM02,
author = {A.~Sherif and A.~L.~C.~Cavalcanti and H.~Moura},
title = {{An Action Semantics for Timed CSPm}},
booktitle = {{6th Brazilian Symposium on Programming Languages}},
year = {2002},
pages = {100-113}
}
@inproceedings{SCM02b,
author = {A.~Sherif and A.~L.~C.~Cavalcanti and H.~Moura},
title = {{Using Abaco to animate a real-time specification language}},
booktitle = {{Action Semantics Workshop - Federated Logic Conference}},
series = {BRICS Notes Series},
year = {2002}
}
@inproceedings{SWC02,
author = {A.~C.~A.~Sampaio and J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
title = {{Refinement in \textsf{\emph{Circus}}}},
booktitle = {{FME 2002: Formal Methods-Getting IT Right}},
year = {2002},
editor = {L.~Eriksson and P.~ A.~Lindsay},
volume = {2391},
series = {Lecture Notes in Computer Science},
pages = {451-470},
publisher = {Springer-Verlag},
url = {papers/SWC02.pdf},
doi = {10.1007/3-540-45614-7_26}
}
@inproceedings{WC02,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
title = {{The Semantics of \textsf{\emph{Circus}}}},
booktitle = {{Formal Specification and Development in Z and B}},
year = {2002},
editor = {D.~Bert and J.~P.~Bowen and M.~C.~Henson and K.~Robinson},
volume = {2272},
series = {Lecture Notes in Computer Science},
pages = {184-203},
publisher = {Springer-Verlag},
url = {papers/WC02.pdf},
doi = {10.1007/3-540-45648-1_10}
}
@article{CSW03,
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
title = {{A Refinement Strategy for \textsf{\emph{Circus}}}},
journal = {Formal Aspects of Computing},
year = {2003},
volume = {15},
pages = {146-181},
number = {2 - 3},
url = {papers/CSW03.pdf},
doi = {10.1007/s00165-003-0006-5}
}
@article{CW03,
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{Predicate Transformers in the Semantics of \textsf{\emph{Circus}}}},
journal = {IEE Proceedings Software},
year = {2003},
volume = {150},
pages = {85-94},
number = {1},
booktitle = {{Communicating Processing Architectures}},
publisher = {IOS Press},
url = {papers/CW03.pdf},
doi = {10.1049/ip-sen:20030131}
}
@inproceedings{DCS03,
author = {A.~A.~Duran and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{A Strategy for Compiling Classes, Inheritance, and Dynamic Binding}},
booktitle = {{Formal Methods}},
year = {2003},
editor = {K.~Araki and S.~Gnesi and D.~Mandrioli},
volume = {2805},
series = {Lecture Notes in Computer Science},
pages = {301-320},
publisher = {Springer-Verlag},
url = {papers/DSC03.pdf},
doi = {10.1007/978-3-540-45236-2_18}
}
@inproceedings{FNC03,
author = {A.~F.~Freitas and C.~M.~P.~Nascimento and A.~L.~C.~Cavalcanti},
title = {{A Refinement Tool for Z}},
booktitle = {International Conference on Formal Engineering Methods},
year = {2003},
editor = {J.~S.~Dong and J.~C.~P.~Woodcock},
volume = {2885},
series = {Lecture Notes in Computer Science},
pages = {396-415},
publisher = {Springer-Verlag},
doi = {10.1007/978-3-540-39893-6_23}
}
@article{OCW03,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{ArcAngel: A Tactic Language for Refinement}},
journal = {Formal Aspects of Computing},
year = {2003},
volume = {15},
pages = {28-47},
number = {1},
doi = {10.1007/s00165-003-0003-8},
url = {papers/OCW03.pdf}
}
@article{BSCC04,
author = {P.~H.~M.~Borba and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti and M.~L.~Corn\'elio},
title = {{Algebraic Reasoning for Object-Oriented Programming}},
journal = {Science of Computer Programming},
year = {2004},
volume = {52},
pages = {53-100},
url = {papers/BSCC04.pdf},
doi = {10.1016/j.scico.2004.03.003}
}
@inproceedings{CCS04,
author = {M.~A.~Corn\'elio and A.~L.~C.~Cavalcanti and A.~C.~A.Sampaio},
title = {{Refactoring Towards a Layered Architecture}},
booktitle = {{Brazilian Symposium on Formal Methods}},
year = {2004},
pages = {199-216},
doi = {10.1016/j.entcs.2005.03.015},
volume = {95},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier}
}
@proceedings{CM04,
title = {WMF 2003:~6th Brazilian Workshop on Formal Methods},
year = {2004},
editor = {A.~L.~C.~Cavalcanti and P.~Machado},
volume = {95},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier}
}
@inproceedings{OXC04,
author = {M.~V.~M.~Oliveira and M.~A.~Xavier and A.~L.~C.~Cavalcanti},
title = {{Refine and Gabriel: Support for Refinement and Tactics}},
booktitle = {IEEE International Conference on Software Engineering and Formal Methods},
year = {2004},
editor = {J.~R.~Cuellar and Z.~Liu},
pages = {310-319},
month = {September},
publisher = {IEEE Computer Society Press},
url = {papers/OXC04.pdf},
doi = {10.1109/SEFM.2004.1347535}
}
@inproceedings{OC04,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti},
title = {{From \textsf{\emph{Circus}} to JCSP}},
booktitle = {International Conference on Formal Engineering Methods},
year = {2004},
editor = {J.~Davies et al.},
volume = {3308},
series = {Lecture Notes in Computer Science},
pages = {320-340},
month = {November},
publisher = {Springer-Verlag},
url = {papers/OC04.pdf},
doi = {10.1007/978-3-540-30482-1_29}
}
@inproceedings{OCW04,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{Refining Industrial Scale Systems in \textsf{\emph{Circus}}}},
booktitle = {Communicating Process Architectures},
year = {2004},
editor = {I.~East and J.~Martin and P.~Welch and D.~Duce and M.~Green},
volume = {62},
series = {Concurrent Systems Engineering Series},
pages = {281-309},
month = {September},
publisher = {IOS Press},
url = {papers/OCW04.pdf}
}
@inproceedings{WC04,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
title = {{A Tutorial Introduction to Designs in Unifying Theories of Programming}},
booktitle = {{IFM 2004: Integrated Formal Methods}},
year = {2004},
editor = {E.~A.~Boiten and J.~Derrick and G.~Smith},
volume = {2999},
series = {Lecture Notes in Computer Science},
pages = {40-66},
publisher = {Springer-Verlag},
note = {Invited tutorial.},
url = {papers/WC04.pdf},
doi = {10.1007/978-3-540-24756-2_4}
}
@inproceedings{CCO05,
author = {A.~L.~C.~Cavalcanti and P.~Clayton and C.~O'Halloran},
title = {{Control Law Diagrams in \textsf{\emph{Circus}}}},
booktitle = {{FM 2005:~Formal Methods}},
year = {2005},
editor = {J.~Fitzgerald and I.~J.~Hayes and A.~Tarlecki},
volume = {3582},
series = {Lecture Notes in Computer Science},
pages = {253-268},
publisher = {Springer-Verlag},
url = {papers/CCO05.pdf},
doi = {10.1007/11526841_18}
}
@article{CSW05,
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
title = {{Unifying Classes and Processes}},
journal = {Software and System Modelling},
year = {2005},
volume = {4},
pages = {277-296},
number = {3},
url = {papers/CSW05.pdf},
doi = {10.1007/s10270-005-0085-2}
}
@inproceedings{CW05,
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{Angelic Nondeterminism and Unifying Theories of Programming }},
booktitle = {{REFINE 2005}},
year = {2005},
editor = {J.~Derrick and E.~Boiten},
volume = {137},
series = {Eletronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2005.04.024}
}
@article{OCW05,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{Formal development of industrial-scale systems}},
journal = {Innovations in Systems and Software Engineering},
year = {2005},
volume = {1},
pages = {126-147},
number = {2},
booktitle = {{Innovations in Systems and Software Engineering - A NASA Journal}},
publisher = {Springer-Verlag},
url = {papers/OCW05.pdf},
doi = {10.1007/s11334-005-0014-0}
}
@inproceedings{SHCS05,
author = {A.~Sherif and J.~He and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{A Framework for Specification and Validation of Real-Time Systems Using \textsf{\emph{Circus}} Actions}},
booktitle = {International Colloquium on Theoretical Aspects of Computing},
volume = 3407,
editor = {Z.~Liu and K.~Araki},
year = {2005},
pages = {478-493},
publisher = {Springer-Verlag},
series = {Lecture Notes in Computer Science},
doi = {10.1007/978-3-540-31862-0_34}
}
@inproceedings{WCF05,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti and L.~Freitas},
title = {{Operational Semantics for Model-Checking \textsf{\emph{Circus}}}},
booktitle = {{Formal Methods}},
year = {2005},
editor = {J.~Fitzgerald and I.~J.~Hayes and A.~Tarlecki},
volume = {3582},
series = {Lecture Notes in Computer Science},
pages = {237-252},
publisher = {Springer-Verlag},
url = {papers/WCF05.pdf},
doi = {10.1007/11526841_17}
}
@inproceedings{XC05,
author = {M.~A.~Xavier and A.~L.~C.~Cavalcanti},
title = {{Mechanised Refinement of Procedures}},
booktitle = {{Brazilian Symposium on Formal Methods}},
year = {2005},
pages = {47-62},
doi = {10.1016/j.entcs.2007.03.015}
}
@inproceedings{CC06,
author = {A.~L.~C.~Cavalcanti and P.~Clayton},
title = {{Verification of Control Systems using \textsf{\emph{Circus}}}},
pages = {269-278},
booktitle = {{11th IEEE International Conference on Engineering of Complex Computer Systems}},
year = {2006},
publisher = {IEEE Computer Society},
url = {papers/CC06.pdf},
doi = {0.1109/ICECCS.2006.1690376}
}
@book{CSW06,
editor = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
title = {{Refinement Techniques in Software Engineering}},
year = {2006},
volume = {3167},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@book{BCC06,
editor = {K.~Barkaoui and A.~L.~C.~Cavalcanti and A.~Cerone},
title = {{Theoretical Aspects of Computing}},
year = {2006},
volume = {4281},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@inproceedings{CSW06a,
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
title = {{Refinement: An Overview}},
booktitle = {{Refinement Techniques in Software Engineering}},
year = {2006},
volume = {3167},
series = {Lecture Notes in Computer Science},
pages = {1-17},
publisher = {Springer-Verlag},
url = {papers/CSW06.pdf},
doi = {10.1007/11889229_1}
}
@inproceedings{CW06,
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{A Tutorial Introduction to CSP in Unifying Theories of Programming}},
booktitle = {{Refinement Techniques in Software Engineering}},
year = {2006},
volume = {3167},
series = {Lecture Notes in Computer Science},
pages = {220-268},
url = {papers/CW06.pdf},
publisher = {Springer-Verlag},
doi = {10.1007/11889229_6}
}
@article{CWD06,
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and S.~Dunne},
title = {{Angelic Nondeterminism in the Unifying Theories of Programming}},
journal = {Formal Aspects of Computing},
volume = {18},
pages = {288-307},
number = {3},
year = {2006},
url = {papers/CWD06.pdf},
doi = {10.1007/s00165-006-0001-8}
}
@inproceedings{CHW06,
author = {A.~L.~C.~Cavalcanti and W.~Harwood and J.~C.~P.~Woodcock},
title = {{Pointers and Records in the Unifying Theories of Programming}},
pages = {200-216},
booktitle = {{Unifying Theories of Programming}},
year = {2006},
editor = {S.~Dunne and B.~Stoddart},
series = {Lecture Notes in Computer Science},
volume = {4010},
publisher = {Springer-Verlag},
url = {papers/CHW06.pdf},
doi = {10.1007/11768173_12}
}
@inproceedings{FC06,
author = {A.~F.~Freitas and A.~L.~C.~Cavalcanti},
title = {{Automatic Translation from \textsf{\emph{Circus}} to Java}},
pages = {115-130},
booktitle = {{Formal Methods}},
year = {2006},
editor = {J.~Misra and T.~Nipkow and E.~Sekerinski},
series = {Lecture Notes in Computer Science},
volume = {4085},
publisher = {Springer-Verlag},
url = {papers/FC06.pdf},
doi = {10.1007/11813040_9}
}
@inproceedings{FCW06,
author = {L.~J.~S.~Freitas and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{Taking our own medicine: applying the refinement calculus to state-rich refinement model checking}},
pages = {697-716},
booktitle = {{International Conference on Formal Engineering Methods}},
year = {2006},
editor = {Z.~Liu and J.~He},
series = {Lecture Notes in Computer Science},
volume = {4260},
publisher = {Springer-Verlag},
url = {papers/FCW06.pdf},
doi = {10.1007/11901433_38}
}
@article{FWC06,
author = {L.~J.~S.~Freitas and J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
title = {State-rich model checking},
pages = {49-64},
journal = {Innovations in Systems and Software Engineering},
year = {2006},
volume = {2},
number = {1},
publisher = {Springer},
url = {papers/FWC06.pdf},
doi = {10.1007/s11334-006-0021-9}
}
@inproceedings{OCW06,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{Unifying Theories in ProofPower-Z}},
pages = {123-140},
booktitle = {{Unifying Theories of Programming}},
year = {2006},
editor = {S.~Dunne and B.~Stoddart},
series = {Lecture Notes in Computer Science},
volume = {4010},
publisher = {Springer-Verlag},
url = {papers/OCW06.pdf},
doi = {10.1007/11768173_8}
}
@inproceedings{OCW06b,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{A denotational semantics for \textsf{\emph{Circus}}}},
booktitle = {{REFINE'2006}},
year = {2006},
editor = {B.~Aichernig and J.~Derrick},
series = {Eletronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
doi = {10.1016/j.entcs.2006.08.047}
}
@inproceedings{SCS06,
author = {T.~L.~V.~L.~Santos and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{Object Orientation in the UTP}},
pages = {18-37},
booktitle = {{Unifying Theories of Programming}},
year = {2006},
editor = {S.~Dunne and B.~Stoddart},
series = {Lecture Notes in Computer Science},
volume = {4010},
publisher = {Springer-Verlag},
url = {papers/SCS06.pdf},
doi = {10.1007/11768173_2}
}
@inproceedings{SCTW06,
author = {S.~Schneider and A.~L.~C.~Cavalcanti and H.~Treharne and J.~C.~P.~Woodcock},
title = {{A Layered Behavioural Model of Platelets}},
pages = {98-106},
booktitle = {{11th IEEE International Conference on Engineering of Complex Computer Systems}},
year = {2006},
publisher = {IEEE Computer Society},
url = {papers/SCTW06.pdf},
doi = {10.1109/ICECCS.2006.1690359}
}
@inproceedings{XCS06,
author = {M.~A.~Xavier and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{Type Checking \textsf{\emph{Circus}} Specifications}},
pages = {105-120},
booktitle = {{Brazilian Symposium on Formal Methods}},
year = {2006},
editor = {A.~M.~Moreira and L.~Ribeiro},
doi = {10.1016/j.entcs.2007.08.027}
}
@inproceedings{AWC07,
author = {E.~G.~Aydal and J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
title = {Goal-Oriented Automatic Test Case Generators for MC/DC Compliancy},
booktitle = {International Conference on Software and Data Technologies},
year = {2007},
pages = {290-295},
publisher = {SciTePress},
organization = {INSTICC},
doi = {10.5220/0001324002900295},
isbn = {978-989-8111-06-7},
volume = {2}
}
@inproceedings{CG07,
author = {A.~L.~C.~Cavalcanti and M.-C.~Gaudel},
title = {{Testing for Refinement in CSP}},
booktitle = {{9th International Conference on Formal Engineering Methods}},
year = {2007},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {4789},
pages = {151-170},
url = {papers/CG07.pdf},
doi = {10.1007/978-3-540-76650-6_10}
}
@inproceedings{FWC07,
author = {L.~J.~S.~Freitas and J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti },
title = {{An Architecture for \textsf{\emph{Circus}} Tools}},
booktitle = {{Brazilian Symposium on Formal Methods}},
year = {2007},
editor = {A.~C.~V.~Melo and A.~Moreira},
url = {papers/FWC07.pdf},
pages = {6-21}
}
@proceedings{BCSW07,
editor = {P.~H.~M.~Borba and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and J.~C.~P.~Woodcock},
title = {Testing Techniques in Software Engineering},
series = {Lecture Notes in Computer Science},
volume = {6153},
publisher = {Springer},
year = {2010}
}
@article{OC08,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti},
booktitle = {{International Refinement Workshop}},
journal = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier B. V.},
title = {{ArcAngelC: a Refinement Tactic Language for \textsf{\emph{Circus}}}},
year = {2008},
volume = {\textbf{214C}},
pages = {203-229},
url = {papers/OC08.pdf},
doi = {10.1016/j.entcs.2008.06.010}
}
@inproceedings{HCW08,
author = {W.~Harwood and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{A Theory of Pointers for the UTP}},
pages = {141-155},
booktitle = {{Theoretical Aspects of Computing}},
year = {2008},
editor = {J.~S.~Fitzgerald and A.~E.~Haxthausen and H.~Yenigun},
series = {Lecture Notes in Computer Science},
volume = {5160},
publisher = {Springer-Verlag},
url = {papers/HCW08.pdf},
doi = {10.1007/978-3-540-85762-4_10}
}
@inproceedings{Cav08,
author = {A.~L.~C.~Cavalcanti},
title = {{Stateflow diagrams in \textsf{\emph{Circus}}}},
booktitle = {{SBMF 2008:~Brazilian Symposium on Formal Methods}},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier B. V.},
year = {2008},
editor = {P.~Machado},
note = {Invited paper},
url = {papers/Cav08.pdf},
doi = {10.1016/j.entcs.2009.05.043}
}
@inproceedings{ZC08a,
author = {F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {{Mechanical Reasoning about Families of UTP Theories}},
booktitle = {{SBMF 2008:~Brazilian Symposium on Formal Methods}},
journal = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier B. V.},
year = {2008},
editor = {P.~Machado},
note = {Best paper award},
doi = {10.1016/j.entcs.2009.05.055}
}
@book{BBCC08,
editor = {K.~Barkaoui and M.~Broy and A.~L.~C.~Cavalcanti and A.~Cerone},
title = {Formal Aspects of Computing},
volume = {20(4-5)},
year = 2008,
note = {Special issue. Guest editors.},
publisher = {Springer}
}
@book{BC09,
editor = {K.~Breitman and A.~L.~C.~Cavalcanti},
title = {{Formal Methods and Software Engineering}},
year = {2009},
volume = {5885},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@book{CD09,
editor = {A.~L.~C.~Cavalcanti and D.~R.~Dams},
title = {{FM 2009:~Formal Methods}},
year = {2009},
volume = {5850},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@article{OCW09,
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {{A UTP Semantics for \textsf{\emph{Circus}}}},
journal = {Formal Aspects of Computing},
year = {2009},
volume = {21},
number = {1-2},
pages = {3-32},
url = {papers/OCW09.pdf},
doi = { 10.1007/s00165-007-0052-5}
}
@inproceedings{ZC08b,
author = {F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {{Encoding \textsf{\emph{Circus}} Programs in ProofPower-Z}},
booktitle = {{Unifying Theories of Programming}},
year = {2009},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
url = {papers/ZC08b.pdf},
doi = {10.1007/978-3-642-14521-6_13}
}
@inproceedings{ZC09,
author = {F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {{Mechanised Translation of Control Law Diagrams into \textsf{\emph{Circus}}}},
booktitle = {{Integrated Formal Methods}},
year = {2009},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
pages = {151-166},
volume = 5423,
editor = {M.~Leuschel and H.~Wehrheim},
url = {papers/ZC09.pdf},
doi = {10.1007/978-3-642-00255-7_11}
}
@article{ZOC09,
title = {{Supporting ArcAngel in ProofPower}},
journal = {Electronic Notes in Theoretical Computer Science},
volume = {259},
pages = {225-243},
year = {2009},
note = {14th BCS-FACS Refinement Workshop (REFINE 2009)},
author = {F.~Zeyda and M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti},
doi = {10.1016/j.entcs.2009.12.027i}
}
@incollection{PWBC10,
author = {R.~F.~Paige and J.~C.~P.~Woodcock and P.~J.~Brooke and A.~L.~C.~Cavalcanti},
title = {Programming Phase: Formal Methods},
booktitle = {Encyclopedia of Software Engineering},
year = {2010},
pages = {772-785},
publisher = {John Wiley and Sons, Inc.}
}
@inproceedings{VZC10,
author = {M.~Vernon and F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {{Communication Systems in ClawZ}},
booktitle = {{Abstract State Machines, Alloy, B, and Z}},
year = {2010},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {5977},
pages = {334-348},
url = {papers/VZC10.pdf},
doi = {10.1007/978-3-642-11811-1_25}
}
@inproceedings{ZC10,
author = {F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {{Automating Refinement of \textsf{\emph{Circus}} Programs}},
booktitle = {{Brazilian Symposium on Formal Methods}},
year = {2010},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
url = {papers/ZC10.pdf},
doi = {10.1007/978-3-642-19829-8_18}
}
@article{DCS10,
author = {A.~Duran and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{An Algebraic Approach to the Design of Compilers for Object-oriented Languages}},
journal = {Formal Aspects of Computing},
year = {2010},
volume = 22,
number = 5,
pages = {489-535},
url = {papers/DCS10.pdf},
doi = {10.1007/s00165-009-0124-9}
}
@article{SCJS10,
author = {A.~Sherif and A.~L.~C.~Cavalcanti and J.~He and A.~C.~A.~Sampaio},
title = {{A process algebraic framework for specification and validation of real-time systems}},
journal = {Formal Aspects of Computing},
year = {2010},
volume = {22},
number = {2},
pages = {153-191},
url = {papers/SCHS10.pdf},
doi = {10.1007/s00165-009-0119-6}
}
@article{CCS10,
author = {M.~Corn\'elio and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{Sound Refactorings}},
journal = {Science of Computer Programming},
year = {2010},
volume = 75,
number = 3,
pages = {106-133},
url = {papers/CCS10.pdf},
doi = {10.1016/j.scico.2009.10.001}
}
@book{CDGW10,
editor = {A.~L.~C.~Cavalcanti and D.~Deharbe and M.-C.~Gaudel and J.~C.~P.~Woodcock},
title = {{Theoretical Aspects of Computing}},
year = {2010},
volume = {6255},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@inproceedings{CG10a,
author = {A.~L.~C.~Cavalcanti and M.-C.~Gaudel},
title = {{A note on traces refinement and the $conf$ relation in the Unifying Theories of Programming}},
booktitle = {{Unifying Theories of Programming}},
year = {2010},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {5713},
editor = {A.~Butterfield},
url = {papers/CG10a.pdf},
doi = {10.1007/978-3-642-14521-6_4}
}
@inproceedings{CG10b,
author = {A.~L.~C.~Cavalcanti and M.-C.~Gaudel},
title = {{Specification Coverage for Testing in \textsf{\emph{Circus}}}},
booktitle = {{Unifying Theories of Programming}},
pages = {1-45},
year = {2010},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
volume = {6445},
editor = {S.~Qin},
url = {papers/CG10b.pdf},
doi = {10.1007/978-3-642-16690-7_1}
}
@inproceedings{MC11a,
title = {{Refinement-based verification of sequential implementations of Stateflow charts}},
booktitle = {Refinement Workshop},
year = {2011},
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti},
series = {Electronic Notes in Theoretical Computer Science},
publisher = {Elsevier},
url = {papers/MC11a.pdf},
doi = {10.4204/EPTCS.55},
editor = {J.~Derrick and E.~Boiten and S.~Reeves}
}
@inproceedings{CWW11,
author = { A.~L.~C.~Cavalcanti and A.~Wellings and J.~C.~P.~Woodcock},
title = {{The Safety-critical Java Memory Model: a formal account}},
booktitle = {Formal Methods},
series = {Lecture Notes in Computer Science},
editor = {M.~Butler and W.~Schulte},
year = {2011},
volume = {6664},
publisher = {Springer-Verlag},
pages = {246-261},
url = {papers/CWW11.pdf},
doi = {10.1007/978-3-642-21437-0_20}
}
@inproceedings{ZCW11,
author = {F.~Zeyda and A.~L.~C.~Cavalcanti and A.~Wellings},
title = {{The Safety-critical Java Mission Model: a formal account}},
year = {2011},
booktitle = {International Conference on Formal Engineering Methods},
series = {Lecture Notes in Computer Science},
url = {papers/ZCW11.pdf},
volume = {6991},
pages = {49-65},
doi = {10.1007/978-3-642-24559-6_6}
}
@inproceedings{CWWWZ11,
author = {A.~L.~C.~Cavalcanti and A.~Wellings and J.~C.~P.~Woodcock and K.~Wei and F.~Zeyda},
title = {{Safety-Critical Java in \textsf{\emph{Circus}}}},
booktitle = {{9th Workshop on Java Technologies for Real-Time and Embedded System}},
series = {ACM Digital Library},
publisher = {ACM},
editor = {A.~P.~Ravn},
year = {2011},
url = {papers/CWWWZ11.pdf},
doi = {10.1145/2043910.2043915}
}
@inproceedings{CGH11,
author = {A.~L.~C.~Cavalcanti and M.-C.~Gaudel and R.~M.~Hierons},
title = {{Conformance Relations for Distributed Testing based on CSP}},
booktitle = {{IFIP International Conference on Testing Software and Systems}},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag},
editor = {B.~Wolff and F.~Zaidi},
year = {2011},
url = {papers/CGH11.pdf},
doi = {10.1007/978-3-642-24580-0_5}
}
@article{CG11,
author = {A.~L.~C.~Cavalcanti and M.-C.~Gaudel},
title = {{Testing for Refinement in \textsf{\emph{Circus}}}},
journal = {Acta Informatica},
volume = 48,
number = 2,
year = {2011},
pages = {97-147},
url = {papers/CG11.pdf},
doi = {10.1007/s00236-011-0133-z}
}
@article{CCO11,
author = {A.~L.~C.~Cavalcanti and P.~Clayton and C.~O'Halloran},
title = {{From Control Law Diagrams to Ada via \textsf{\emph{Circus}}}},
year = {2011},
journal = {Formal Aspects of Computing},
volume = {23},
number = {4},
pages = {465-512},
url = {papers/CCO11.pdf},
doi = {10.1007/s00165-010-0170-3}
}
@article{OZC11,
title = {A Tactic Language for Refinement of State-rich Concurrent Specifications},
journal = {Science of Computer Programming},
year = {2011},
volume = 76,
number = 9,
pages = {792-833},
author = {M.~V.~M.~Oliveira and F.~Zeyda and A.~L.~C.~Cavalcanti},
url = {papers/OZC11.pdf},
doi = {10.1016/j.scico.2010.11.012}
}
@book{CD11a,
editor = {A.~L.~C.~Cavalcanti and D.~Dams},
title = {Formal Aspects of Computing},
volume = {23(6)},
year = 2011,
note = {Special issue. Guest editors.},
publisher = {Springer}
}
@book{CD11b,
editor = {A.~L.~C.~Cavalcanti and D.~Dams},
title = {Formal Methods in System Design},
volume = {37(2-3)},
year = 2011,
note = {Special issue. Guest editors.},
publisher = {Springer}
}
@article{ZC12,
author = {F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {{Mechanical Reasoning about Families of UTP Theories}},
journal = {Science of Computer Programming},
year = {2012},
volume = {77},
number = {4},
pages = {444-479},
url = {papers/ZC12.pdf},
doi = {10.1016/j.scico.2010.02.010}
}
@article{ZOC12,
title = {Mechanised support for sound refinement tactics},
journal = {Formal Aspects of Computing},
year = {2012},
volume = 24,
number = 1,
pages = {127-160},
author = {F.~Zeyda and M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti},
url = {papers/ZOC12.pdf},
doi = {10.1007/s00165-011-0218-z}
}
@incollection{MZC12,
author = {C.~Marriott and F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {{A Tool Chain for the Automatic Generation of \textsf{\emph{Circus}} Specifications of Simulink Diagrams}},
booktitle = {Abstract State Machines, Alloy, B, VDM, and Z},
series = {Lecture Notes in Computer Science},
editor = {J.~Derrick and J.~Fitzgerald and S.~Gnesi and S.~Khurshid and M.~Leuschel and S.~Reeves and E.~Riccobene},
publisher = {Springer},
pages = {294-307},
volume = {7316},
year = {2012},
url = {papers/MZC12.pdf},
doi = {10.1007/978-3-642-30885-7_21i}
}
@article{MC12,
title = {{Refinement-oriented models of Stateflow charts}},
year = {2012},
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti},
journal = {Science of Computer Programming},
publisher = {Elsevier},
volume = 77,
number = {10-11},
pages = {1151-1177},
url = {papers/MC12.pdf},
doi = {10.1016/j.scico.2011.07.007}
}
@book{Cav12,
editor = {A.~L.~C.~Cavalcanti},
title = {Science of Computer Programming},
volume = {77(12)},
year = 2012,
note = {Special issue. Guest editor.},
publisher = {Elsevier}
}
@book{CD12,
editor = {A.~L.~C.~Cavalcanti and D.~D\'eharbe},
title = {Theoretical Computer Science},
volume = {455},
year = 2012,
note = {Special issue. Guest editors.},
publisher = {Elsevier}
}
@inproceedings{SWC12,
author = {N.~K.~Singh and A.~J.~Wellings and A.~L.~C.~Cavalcanti},
title = {The cardiac pacemaker case study and its implementation in safety-critical {Java and Ravenscar Ada}},
booktitle = {10th International Workshop on Java Technologies for Real-time and Embedded Systems},
year = {2012},
pages = {62-71},
publisher = {ACM},
url = {papers/SWC12.pdf},
doi = {10.1007/s00165-012-0253-4}
}
@inproceedings{WCFLMP12,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti and J.~Fitzgerald and P.~G.~Larsen and A.~Miyazawa and S.~Perry},
title = {{Features of CML: a Formal Modelling Language for Systems of Systems}},
booktitle = {7th International Conference on Systems of Systems Engineering},
volume = {6},
series = {IEEE Systems Journal},
publisher = {IEEE},
year = {2012},
url = {papers/WCFLMP12.pdf},
doi = {10.1109/SYSoSE.2012.6384144}
}
@article{CWW13,
title = {{The Safety-Critical Java memory model formalised}},
journal = {Formal Aspects of Computing},
year = {2013},
author = {A.~L.~.C~Cavalcanti and A.~Wellings and J.~C.~P.~Woodcock},
volume = {25},
number = {1},
pages = {37-57},
url = {papers/CWW13.pdf},
doi = {10.1007/s00165-012-0253-4}
}
@inproceedings{CH13,
author = {A.~L.~C.~Cavalcanti and R.~M.~Hierons},
title = {{Testing with Inputs and Outputs in CSP}},
booktitle = {Fundamental Approaches to Software Engineering},
year = {2013},
series = {Lecture Notes in Computer Science},
volume = {7793},
pages = {359-374},
url = {papers/CH13.pdf},
doi = {10.1007/978-3-642-37057-1_26}
}
@inproceedings{RC13,
author = {P.~Ribeiro and A.~L.~C.~Cavalcanti},
title = {Designs with Angelic Nondeterminism},
pages = {71-78},
booktitle = {7th International Symposium on Theoretical Aspects of Software Engineering},
publisher = {IEEE},
year = {2013},
url = {papers/RC13.pdf},
doi = {10.1109/TASE.2013.18}
}
@article{CZWWW13,
author = {A.~L.~C.~Cavalcanti and F.~Zeyda and A.~Wellings and J.~C.~P.~Woodcock and K.~Wei},
title = {{Safety-critical Java programs from \textsf{\emph{Circus}} models}},
journal = {{Real-Time Systems}},
year = {2013},
volume = {49},
number = {5},
pages = {614-667},
url = {papers/CZWWW13.pdf},
doi = {10.1007/s11241-013-9182-4}
}
@article{OCW13,
year = {2013},
journal = {Formal Aspects of Computing},
volume = {25},
number = {1},
title = {{Unifying theories in ProofPower-Z}},
publisher = {Springer-Verlag},
author = {M.~V.~M.~Oliveira and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
pages = {133-158},
url = {papers/OCW13.pdf},
doi = {10.1007/s00165-007-0044-5}
}
@inproceedings{CMW13,
author = {A.~L.~C.~Cavalcanti and A.~Mota and J.~C.~P.~Woodcock},
title = {Simulink Timed Models for Program Verification},
year = {2013},
pages = {82-99},
editor = {Z.~Liu and J.~C.~P.~Woodcock and H.~Zhu},
booktitle = {Theories of Programming and Formal Methods - Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8051},
url = {papers/CMW13.pdf},
doi = {10.1007/978-3-642-39698-4_6}
}
@inproceedings{MLC13,
author = {A.~Miyazawa and L.~Lima and A.~L.~C.~Cavalcanti},
title = {{Formal Models of SysML Blocks}},
year = {2013},
pages = {249-264},
editor = {L.~Groves and J.~Sun},
booktitle = {15th International Conference on Formal Engineering Methods},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
volume = {8144},
url = {papers/MLC13.pdf},
doi = {10.1007/978-3-642-41202-8_17}
}
@inproceedings{ZC13b,
author = {F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {{Refining SCJ Mission Specifications into Parallel Handler Designs}},
year = {2013},
pages = {52-67},
editor = {J.~Derrick and E.~A.~Boiten and S.~Reeves},
booktitle = {16th International Refinement Workshop},
series = {EPTCS},
volume = {115},
url = {papers/ZC13b.pdf},
doi = {10.4204/EPTCS.115.4}
}
@incollection{ZC13a,
year = {2013},
booktitle = {Unifying Theories of Programming},
volume = {7681},
series = {Lecture Notes in Computer Science},
editor = {B.~Wolff and M.-C.~Gaudel and A.~Feliachi},
title = {{Higher-Order UTP for a Theory of Methods}},
publisher = {Springer},
author = {F.~Zeyda and A.~L.~C.~Cavalcanti},
pages = {204-223},
url = {papers/ZC13a.pdf},
doi = {10.1007/978-3-642-35705-3_10}
}
@inproceedings{WWC13,
author = {K.~Wei and J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti},
title = {{\textsf{\emph{Circus Time}} with Reactive Designs}},
booktitle = {Unifying Theories of Programming},
year = {2013},
series = {Lecture Notes in Computer Science},
volume = {7681},
editor = {B.~Wolff and M.-C.~Gaudel and A.~Feliachi},
publisher = {Springer},
url = {papers/WWC13.pdf},
doi = {10.1007/978-3-642-35705-3_3}
}
@inproceedings{WLC13,
author = {A.~J.~Wellings and M.~Luckcuck and A.~L.~C~Cavalcanti},
title = {{Safety-critical Java level 2: motivations, example applications and issues}},
booktitle = {The 11th International Workshop on Java Technologies for Real-time and Embedded Systems},
year = {2013},
pages = {48-57},
editor = {F.~Siebert and K.~Nilsen},
publisher = {{ACM}},
url = {papers/WLC13.pdf},
doi = {10.1145/2512989.2512991}
}
@article{WBCS13,
author = {A.~J.~Wellings and A.~Burns and A.~L.~C.~Cavalcanti and N.~K.~Singh},
title = {{Programming Simple Reactive Systems in Ada: Premature Program Termination}},
journal = {Ada Letters},
volume = {33},
number = {2},
year = {2013},
pages = {75-86},
publisher = {ACM},
url = {papers/WBCS13.pdf},
doi = {10.1145/2552999.2553008}
}
@article{MC14,
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti},
title = {{Refinement-based verification of implementations of Stateflow charts}},
year = {2014},
journal = {{Formal Aspects of Computing}},
volume = {26},
number = {2},
pages = {367-405},
url = {papers/MC14.pdf},
doi = {10.1007/s00165-013-0291-6}
}
@article{ZLCW14,
author = {F.~Zeyda and L.~Lalkhumsanga and A.~L.~C.~Cavalcanti and A.~Wellings},
title = {{\textsf{\emph{Circus}} Models for Safety-Critical Java Programs}},
journal = {{The Computer Journal}},
volume = {57},
number = {7},
pages = {1046-1091},
year = {2014},
url = {papers/ZLCW14.pdf},
doi = {10.1093/comjnl/bxt060}
}
@inproceedings{CG14,
author = {A.~L.~C.~Cavalcanti and M.-C.~Gaudel},
title = {{Data Flow coverage for \textsf{\emph{Circus}}-based testing}},
year = {2014},
booktitle = {Fundamental Approaches to Software Engineering},
series = {Lecture Notes in Computer Science},
volume = {8441},
pages = {415-429},
url = {papers/CG14.pdf},
doi = {10.1007/978-3-642-54804-8_29}
}
@inproceedings{ZSCS14,
author = {F.~Zeyda and T.~L.~V.~L.~Santos and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {{A modular theory of object orientation in higher-order UTP}},
booktitle = {Formal Methods},
year = {2014},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {8442},
pages = {627-642},
url = {papers/ZSCS14.pdf},
doi = {10.1007/978-3-319-06410-9_42}
}
@inproceedings{MC14a,
author = {C.~Marriott and A.~L.~C.~Cavalcanti},
title = {{SCJ: Memory-safety checking without annotations}},
booktitle = {Formal Methods},
year = {2014},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {8442},
pages = {465-480},
url = {papers/MC14a.pdf},
doi = {10.1007/978-3-319-06410-9_32}
}
@inproceedings{RC14a,
author = {P.~Ribeiro and A.~L.~C.~Cavalcanti},
title = {{Angelicism in the theory of reactive processes}},
booktitle = {Unifying Theories of Programming},
year = {2014},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
url = {papers/RC14a.pdf},
doi = {10.1007/978-3-319-14806-9_3}
}
@inproceedings{FMWCFL14,
author = {S.~Foster and A.~Miyazawa and J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti and J.~Fitzgerald and P.~G.~Larsen},
title = {{An approach for managing semantic heterogeneity in Systems of Systems Engineering}},
booktitle = {9th International Conference on Systems of Systems Engineering},
series = {IEEE Systems Journal},
publisher = {IEEE},
year = {2014},
url = {papers/FMWCFL14.pdf},
doi = {10.1109/SYSOSE.2014.6892473}
}
@inproceedings{WCFFL14,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti and J.~Fitzgerald and S.~Foster and P.~G.~Larsen},
title = {{Contracts in CML}},
booktitle = {6th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
year = {2014},
url = {papers/WCFFL14.pdf},
doi = {10.1007/978-3-662-45231-8_5}
}
@inproceedings{HMCK14,
author = {R.~Hawkins and A.~Miyazawa and A.~L.~C.~Cavalcanti and T.~Kelly and J.~Rowlands},
title = {{Assurance Cases for Block-configurable Software}},
year = {2014},
booktitle = {33rd International Conference on Computer Safety, Reliability and Security},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
url = {papers/HMCKR14.pdf},
doi = {10.1007/978-3-319-10506-2_11}
}
@article{CKOW14,
author = {A.~L.~C.~Cavalcanti and S.~King and C.~O'Halloran and J.~C.~P.~Woodcock},
title = {{Test-Data Generation for Control Coverage by Proof}},
journal = {{Formal Aspects of Computing}},
year = {2014},
volume = 26,
number = 4,
pages = {795-823},
url = {papers/CKOW14.pdf},
doi = {10.1007/s00165-013-0279-2}
}
@incollection{MC14b,
year = {2014},
booktitle = {11th International Conference on Integrated Formal Methods},
series = {Lecture Notes in Computer Science},
editor = {E.~Albert and E.~Sekerinski},
title = {{Formal Refinement in SysML}},
publisher = {Springer},
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti},
pages = {155-170},
url = {papers/MC14b.pdf},
doi = {10.1007/978-3-319-10181-1_10}
}
@inproceedings{RC14b,
author = {P.~Ribeiro and A.~L.~C.~Cavalcanti},
title = {{UTP Designs for Binary Multirelations}},
booktitle = {Theoretical Aspects of Computing},
year = {2014},
pages = {388-405},
editor = {G.~Ciobanu and D.~M{\'{e}}ry},
series = {Lecture Notes in Computer Science},
volume = {8687},
publisher = {Springer},
url = {papers/RC14b.pdf},
doi = {10.1007/978-3-319-10882-7_23}
}
@inproceedings{CCRCS14,
author = {G.~Carvalho and A.~Carvalho and E.~Rocha and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
title = {A Formal Model for Natural-Language Timed Requirements of Reactive Systems},
booktitle = {Formal Methods and Software Engineering},
year = {2014},
pages = {43-58},
editor = {S.~Merz and J.~Pang},
series = {Lecture Notes in Computer Science},
volume = {8829},
publisher = {Springer},
url = {papers/CCRCS14.pdf},
doi = {10.1007/978-3-319-11737-9_4}
}
@article{CG15,
author = {A.~L.~C.~Cavalcanti and M.-C.~Gaudel},
title = {Test Selection for Traces Refinement},
journal = {Theoretical Computer Science},
volume = {563},
number = {0},
pages = {1 - 42},
year = {2015},
url = {papers/CG15.pdf},
doi = {10.1016/j.tcs.2014.08.012}
}
@article{ZC15,
author = {F.~Zeyda and A.~L.~C.~Cavalcanti},
title = {Laws of mission-based programming},
journal = {Formal Aspects of Computing},
year = {2015},
url = {papers/ZC15.pdf},
doi = {10.1007/s00165-014-0317-8},
volume = {27},
number = {2},
pages = {423-472}
}
@incollection{MC15a,
year = {2015},
booktitle = {REFINE Workshop},
title = {{\textsf{\emph{SCJ-Circus}}: a refinement-oriented formal notation for Safety-Critical Java}},
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti},
url = {arxiv.org/pdf/1606.02021}
}
@inproceedings{CBCCMS15,
author = {G.~Carvalho and F.~A.~Barros and A.~Carvalho and A.~L.~C.~Cavalcanti and A.~Mota and A.~C.~A.~Sampaio},
title = {{NAT2TEST} Tool: From Natural Language Requirements to Test Cases Based on {CSP}},
booktitle = {13th International Conference Software Engineering and Formal Methods},
pages = {283-290},
year = {2015},
editor = {R.~Calinescu and B.~Rumpe},
series = {Lecture Notes in Computer Science},
volume = {9276},
publisher = {Springer},
url = {papers/CBCCMS15.pdf},
doi = {10.1007/978-3-319-22969-0_20}
}
@article{LMCCISHLL15,
year = {2017},
volume = {16},
number = {3},
journal = {Software \& Systems Modeling},
title = {{An integrated semantics for reasoning about SysML design models using refinement}},
publisher = {Springer},
author = {L.~Lima and A.~Miyazawa and A.~L.~C.~Cavalcanti and M.~Corn\'elio and J.~Iyoda and A.~C.~A.~Sampaio and R.~Hains and A.~Larkham and V.~Lewis},
pages = {1-28},
url = {papers/LMCCISHLL15.pdf},
doi = {10.1007/s10270-015-0492-y}
}
@inproceedings{BCWF15,
author = {J.~Baxter and A.~L.~C.~Cavalcanti and A.~J.~Wellings and L.~Freitas},
title = {{Safety-Critical Java Virtual Machine Services}},
booktitle = {13th International Workshop on Java Technologies for Real-time and Embedded Systems},
pages = {7:1-7:10},
year = {2015},
editor = {L.~Ziarek},
publishier = {{ACM}},
url = {papers/BCWF15.pdf},
doi = {10.1145/2822304.2822307}
}
@inproceedings{CHPW15,
author = {A.~L.~C.~Cavalcanti and W.-L. Huang and J.~Peleska and J.~C.~P.~Woodcock},
title = {{CSP and Kripke Structures}},
booktitle = {Theoretical Aspects of Computing},
pages = {505-523},
year = {2015},
editor = {M.~Leucker and C.~Rueda and F.~D.~Valencia},
publisher = {Springer},
url = {papers/CHPW15.pdf},
doi = {10.1007/978-3-319-25150-9_29}
}
@inproceedings{MC15b,
booktitle = {Brazilian Symposium on Formal Methods},
title = {{Refinement strategies for Safety-Critical Java}},
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti},
year = {2015},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {M.~L.~Corn\'elio},
url = {papers/MC15b.pdf},
doi = {10.1007/978-3-319-29473-5_6}
}
@inproceedings{WCW15,
booktitle = {Brazilian Symposium on Formal Methods},
title = {{Mobile CSP}},
author = {J.~C.~P.~Woodcock and A.~J.~Wellings and A.~L.~C.~Cavalcanti},
year = {2015},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {M.~L.~Corn\'elio},
url = {papers/WWC15.pdf},
doi = {10.1007/978-3-319-29473-5_3}
}
@inproceedings{Cav15,
author = {A.~L.~C.~Cavalcanti},
editor = {M.~Butler and S.~Conchon and F.~Za{\"{\i}}di},
booktitle = {17th International Conference on Formal Engineering Methods},
title = {{Can Java Ever Be Safe? The hiJaC Project Abstract}},
series = {Lecture Notes in Computer Science},
volume = {9407},
publisher = {Springer},
year = {2015},
note = {Invited}
}
@inproceedings{FBCW16,
booktitle = {Integrated Formal Methods},
title = {{Modelling and verifying a priority scheduler for an SCJ runtime environment}},
author = {L.~Freitas and J.~Baxter and A.~L.~C.~Cavalcanti and A.~Wellings},
year = {2016},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
url = {papers/FBCW16.pdf},
doi = {10.1007/978-3-319-33693-0_5},
editor = {E.~{\'A}brah{\'a}m and M.~Huisman},
pages = {63-78},
volume = 9681
}
@inproceedings{LCW16,
booktitle = {Integrated Formal Methods},
title = {{A Formal Model of the Safety-Critical Java Level 2 Paradigm}},
author = {M.~Luckcuck and A.~L.~C.~Cavalcanti and A.~Wellings},
year = {2016},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
url = {papers/LCW16.pdf},
doi = {10.1007/978-3-319-33693-0_15},
editor = {E.~{\'A}brah{\'a}m and M.~Huisman},
pages = {226-241},
volume = 9681
}
@inproceedings{CWA16,
booktitle = {International Colloquium on Theoretical Aspects of Computing},
title = {{Behavioural Models for FMI Co-simulations}},
editor = {A.~C.~A.~Sampaio and F.~Wang},
author = {A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and N.~Am\'alio},
year = {2016},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
volume = {9965},
pages = {255-273},
url = {papers/CWA16.pdf},
doi = {10.1007/978-3-319-46750-4_15}
}
@inproceedings{APCW16,
booktitle = {International Conference on Formal Engineering Methods},
title = {{Checking SysML Models for Co-Simulation}},
author = {N.~Am\'alio and R.~Payne and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
year = {2016},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
url = {papers/APCW16.pdf},
volume = {10009},
pages = {450-465},
doi = {10.1007/978-3-319-47846-3_28}
}
@inproceedings{COSC16,
booktitle = {International Conference on Formal Engineering Methods},
title = {{Local Livelock Analysis of Component-Based Models}},
author = {M.~Conserva~Filho and M.~V.~M.~Oliveira and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti},
year = {2016},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
pages = {279-295},
url = {papers/COSC16.pdf},
volume = {10009},
doi = {10.1007/978-3-319-47846-3_18}
}
@article{CCS16,
title = {{Modelling Timed Reactive Systems from Natural-Language Requirements}},
journal = {Formal Aspects of Computing},
volume = {28},
number = {5},
pages = {725-765},
year = {2016},
author = {G.~Carvalho and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
url = {papers/CCS16.pdf},
doi = {10.1007/s00165-016-0387-x}
}
@inproceedings{CHNS16,
author = {A.~L.~C.~Cavalcanti and R.~M.~Hierons and S.~Nogueira and A.~C.~A.~Sampaio},
booktitle = {International Symposium on Theoretical Aspects of Software Engineering},
title = {A Suspension-Trace Semantics for {CSP}},
year = {2016},
pages = {3-13},
doi = {10.1109/TASE.2016.9},
url = {papers/CHNS16.pdf},
note = {Invited paper}
}
@article{ACGS17,
title = {{Formal mutation testing for \textsf{\emph{Circus}}}},
journal = {Information and Software Technology },
volume = {81},
pages = {131-153},
year = {2017},
author = {A.~Alberto and A.~L.~C.~Cavalcanti and M.-C.~Gaudel and A.~Simao},
url = {papers/ACGS16.pdf},
doi = {10.1016/j.infsof.2016.04.003}
}
@article{LWC17,
author = {M.~Luckcuck and A.~Wellings and A.~L.~C.~Cavalcanti},
title = {{Safety-Critical Java: level 2 in practice}},
journal = {Concurrency and Computation: Practice and Experience},
doi = {10.1002/cpe.3951},
year = {2017},
volume = 29,
issue = 6
}
@inproceedings{FTCW17,
author = {S.~Foster and B.~Thiele and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
editor = {J.~Bowen and H.~Zhu},
title = {{Towards a UTP Semantics for Modelica}},
booktitle = {6th International Symposium on Unifying Theories of Programming},
year = {2017},
publisher = {Springer},
pages = {44-64},
doi = {10.1007/978-3-319-52228-9_3},
url = {papers/FTCW17.pdf},
volume = 10134,
series = {Lecture Notes in Computer Science}
}
@inproceedings{RCW17,
booktitle = {6th International Symposium on Unifying Theories of Programming},
title = {{A Stepwise Approach to Linking Theories}},
author = {P.~Ribeiro and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
year = {2017},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {J.~Bowen and H.~Zhu},
pages = {134-154},
doi = {10.1007/978-3-319-52228-9_7},
url = {papers/RCW17.pdf},
volume = 10134
}
@inproceedings{CMWWZ17,
booktitle = {Engineering Trustworthy Software Systems},
title = {{Java in the Safety-Critical Domain}},
author = {A.~L.~C.~Cavalcanti and A.~Miyazawa and A.~Wellings and J.~C.~P.~Woodcock and S.~Zhao},
year = {2017},
series = {Lecture Notes in Computer Science},
publisher = {Springer},
editor = {J.~Bowen and Z.~Liu and Z.~Zhang},
pages = {110-150},
doi = {10.1007/978-3-319-56841-6_4},
url = {papers/CMWWZ17.pdf},
volume = 10215
}
@inproceedings{RMLCT17,
author = {P.~Ribeiro and A.~Miyazawa and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis},
editor = {N.~Polikarpova and S.~Schneider},
title = {Modelling and Verification of Timed Robotic Controllers},
booktitle = {Integrated Formal Methods},
year = {2017},
publisher = {Springer},
pages = {18-33},
doi = {10.1007/978-3-319-66845-1_2},
url = {papers/RMLCT17.pdf}
}
@inproceedings{BC17,
author = {J.~Baxter and A.~L.~C.~Cavalcanti},
editor = {N.~Polikarpova and S.~Schneider},
title = {{Algebraic Compilation of Safety-Critical Java Bytecode}},
booktitle = {Integrated Formal Methods},
year = {2017},
publisher = {Springer},
pages = {161-176},
doi = {10.1007/978-3-319-66845-1_11},
url = {papers/BC17.pdf}
}
@inproceedings{CS17,
author = {A.~L.~C.~Cavalcanti and A.~Simao},
title = {Fault-Based Testing for Refinement in {CSP}},
booktitle = {29th {IFIP} {WG} 6.1 International Conference on Testing Software and Systems},
pages = {21-37},
year = {2017},
doi = {10.1007/978-3-319-67549-7_2},
editor = {N.~Yevtushenko and A.~R.~Cavalli and H.~Yenig{\"{u}}n},
series = {Lecture Notes in Computer Science},
volume = {10533},
publisher = {Springer},
url = {papers/CS17.pdf}
}
@incollection{CMPW17,
author = {A.~L.~C.~Cavalcanti and A.~Miyazawa and R.~Payne and J.~Woodcock},
editor = {M.~Mazzara and B.~Meyer},
title = {Sound Simulation and Co-simulation for Robotics},
booktitle = {Present and Ulterior Software Engineering},
year = {2017},
publisher = {Springer International Publishing},
pages = {173-194},
doi = {10.1007/978-3-319-67425-4_11},
url = {papers/CMPW17.pdf}
}
@inproceedings{OCS17,
author = {R.~Otoni and A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio},
editor = {S.~Cavalheiro and J.~Fiadeiro},
title = {{Local Analysis of Determinism for CSP}},
booktitle = {Formal Methods: Foundations and Applications},
year = {2017},
publisher = {Springer International Publishing},
pages = {107-124},
volume = {10623},
series = {Lecture Notes in Computer Science},
doi = {10.1007/978-3-319-70848-5_8},
url = {papers/OCS17.pdf}
}
@inproceedings{MRLCT17,
author = {A.~Miyazawa and P.~Ribeiro and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis},
title = {Automatic Property Checking of Robotic Applications},
year = {2017},
booktitle = {IEEE/RSJ International Conference on Intelligent Robots and Systems},
volume = {},
number = {},
pages = {3869-3876},
doi = {10.1109/IROS.2017.8206238},
url = {papers/MRLCT17.pdf}
}
@inproceedings{FRCGMSC17,
author = {L.~Fernandes and M.~Ribeiro and L.~Carvalho and R.~Gheyi and M.~Mongiovi and A.~Santos and A.~L.~C.~Cavalcanti and F.~Ferrari and J.~C.~C.~Maldonado},
title = {Avoiding Useless Mutants},
booktitle = {16th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences},
series = {ACM SIGPLAN Notices - GPCE 2017},
volume = {52},
number = {12},
year = {2017},
pages = {187-198},
doi = {10.1145/3170492.3136053},
publisher = {ACM}
}
@book{LSC17,
editor = {L.~Petrucci and C.~Seceleanu and A.~L.~C.~Cavalcanti},
title = {{Critical Systems: Formal Methods and Automated Verification}},
year = {2017},
volume = {10471},
series = {Lecture Notes in Computer Science},
publisher = {Springer-Verlag}
}
@article{COSC18,
title = {Compositional and Local Livelock Analysis for {CSP}},
journal = {Information Processing Letters },
volume = {133},
pages = {21-25},
year = {2018},
doi = {doi.org/10.1016/j.ipl.2017.12.011},
author = {M.~S.~Conserva Filho and M.~V.~M.~Oliveira and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti}
}
@article{FCWZ18,
title = {Unifying theories of time with generalised reactive processes },
journal = {Information Processing Letters },
volume = {135},
number = {},
pages = {47-52},
year = {2018},
doi = {doi.org/10.1016/j.ipl.2018.02.017},
author = {S.~Foster and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and F.~Zeyda}
}
@inproceedings{ZOFC18,
author = {F.~Zeyda and J.~Ouy and S.~Foster and A.~L.~C.~Cavalcanti},
title = {Formalising Cosimulation Models},
booktitle = {Software Engineering and Formal Methods - {SEFM} 2017 Collocated Workshops},
pages = {453-468},
doi = {10.1007/978-3-319-74781-1_31},
editor = {A.~Cerone and M.~Roveri},
series = {Lecture Notes in Computer Science},
volume = {10729},
publisher = {Springer},
year = {2018},
url = {papers/ZOFC18.pdf}
}
@inbook{LMRCWT18,
author = {W.~Li and A.~Miyazawa P.~Ribeiro and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and J.~Timmis},
editor = {R.~Gro{\ss} and A.~Kolling and S.~Berman and E.~Frazzoli and A.~Martinoli and F.~Matsuno and M.~Gauci},
title = {From Formalised State Machines to Implementations of Robotic Controllers},
booktitle = {Distributed Autonomous Robotic Systems: The 13th International Symposium},
year = {2018},
publisher = {Springer International Publishing},
pages = {517-529},
doi = {10.1007/978-3-319-73008-0_36},
url = {arxiv.org/abs/1702.01783}
}
@inproceedings{CMSLRT18,
author = {A.~L.~C.~Cavalcanti and A.~Miyazawa and A.~C.~A.~Sampaio and W.~Li and P.~Ribeiro and J.~Timmis},
editor = {C.~A.~Furia and K.~Winter},
title = {Modelling and Verification for Swarm Robotics},
booktitle = {Integrated Formal Methods},
year = {2018},
publisher = {Springer},
pages = {1-19},
doi = {10.1007/978-3-319-98938-9_1},
url = {papers/CMSLRT18.pdf}
}
@inproceedings{FYCW18,
author = {S.~Foster and K.~Ye and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
editor = {J.~Desharnais and W.~Guttmann and S.~Joosten},
title = {{Calculational Verification of Reactive Programs with Reactive Relations and Kleene Algebra}},
booktitle = {Relational and Algebraic Methods in Computer Science},
year = {2018},
publisher = {Springer},
pages = {205-224},
doi = {10.1007/978-3-030-02149-8_13},
url = {papers/FYCW18.pdf}
}
@inproceedings{FBCMW18,
author = {S.~Foster and J.~Baxter and A.~L.~C.~Cavalcanti and A.~Miyazawa and J.~C.~P.~Woodcock},
editor = {K.~Bae and P.~C.~{\"O}lveczky},
title = {{{Automating Verification of State Machines with Reactive Designs and Isabelle/UTP}}},
booktitle = {Formal Aspects of Component Software},
year = {2018},
publisher = {Springer},
address = {Cham},
pages = {137-155},
doi = {10.1007/978-3-030-02146-7_7},
url = {papers/FBCMW18.pdf}
}
@article{RC19,
title = {{Angelic processes for CSP via the UTP}},
journal = {Theoretical Computer Science},
year = {2019},
doi = {10.1016/j.tcs.2018.10.008},
author = {P.~Ribeiro and A.~L.~C.~Cavalcanti},
url = {papers/RC18.pdf},
volume = {756},
pages = {19-63}
}
@article{CSMRCDLT19,
title = {Verified simulation for robotics},
journal = {Science of Computer Programming},
year = {2019},
doi = {doi.org/10.1016/j.scico.2019.01.004},
author = {A.~L.~C.~Cavalcanti and A.~C.~A.~Sampaio and A.~Miyazawa and P.~Ribeiro and M.~Conserva~Filho and A.~Didier and W.~Li and J.~Timmis},
url = {papers/CSMRCD19.pdf},
volume = {174},
pages = {1-37}
}
@article{MRLCTW19,
year = {2019},
volume = {18},
number = {5},
journal = {Software \& Systems Modeling},
title = {{RoboChart: modelling and verification of the functional behaviour of robotic applications}},
publisher = {Springer},
author = {A.~Miyazawa and P.~Ribeiro and W.~Li and A.~L.~C.~Cavalcanti and J.~Timmis and J.~C.~P.~Woodcock},
pages = {3097-3149},
doi = {doi.org/10.1007/s10270-018-00710-z},
url = {rdcu.be/bh7dI}
}
@article{CS19,
author = {A.~L.~C.~Cavalcanti and A.~Simao},
title = {{Fault-based refinement-testing for CSP}},
journal = {Software Quality Journal},
year = {2019},
doi = {10.1007/s11219-018-9431-9},
url = {doi.org/10.1007/s11219-018-9431-9}
}
@article{PHC19,
title = {{Finite complete suites for CSP refinement testing}},
journal = {Science of Computer Programming},
volume = {179},
pages = {1 - 23},
year = {2019},
issn = {0167-6423},
doi = {doi.org/10.1016/j.scico.2019.04.004},
url = {papers/PHC19.pdf},
author = {J.~Peleska and W.-l.~Huang and A.~L.~C.~Cavalcanti}
}
@article{MC19,
title = {{SCJ-Circus: Specification and refinement of Safety-Critical Java programs}},
journal = {Science of Computer Programming},
volume = {181},
pages = {140-176},
year = {2019},
doi = {doi.org/10.1016/j.scico.2019.01.002},
url = {papers/MC19.pdf},
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti and A.~Wellings}
}
@inproceedings{WCFMY19,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti and S.~Foster and A.~Mota and K.~Ye},
editor = {P.~Ribeiro and A.~C.~A.~Sampaio},
title = {{Probabilistic Semantics for RoboChart}},
booktitle = {Unifying Theories of Programming},
year = {2019},
publisher = {Springer},
doi = {doi.org/10.1007/978-3-030-31038-7_5},
url = {papers/WCFMY19.pdf},
pages = {80--105}
}
@inproceedings{CBHL19,
author = {A.~L.~C.~Cavalcanti and J.~Baxter and R.~M.~Hierons and R.~Lefticaru},
editor = {D.~Beyer and C.~Keller},
title = {{Testing Robots using CSP}},
booktitle = {Tests and Proofs},
year = {2019},
publisher = {Springer},
doi = {doi.org/10.1007/978-3-030-31157-5_2},
url = {papers/CBHL19.pdf},
pages = {21--38}
}
@article{FCCWZ20,
author = {S.~Foster and A.~L.~C.~Cavalcanti and S.~Canham and J.~C.~P.~Woodcock and F.~Zeyda},
title = {Unifying theories of reactive design contracts},
journal = {Theoretical Computer Science},
volume = {802},
pages = {105 -- 140},
year = {2020},
url = {papers/FCCWZ20.pdf},
doi = {10.1016/j.tcs.2019.09.017}
}
@article{CHN20,
author = {A.~L.~C.~Cavalcanti and R.~Hierons and S.~Nogueira},
title = {{Inputs and outputs in CSP: a model and a testing theory}},
journal = {ACM Transactions on Computational Logic},
year = {2020},
url = {papers/CHN20.pdf},
doi = {10.1145/3379508}
}
@inproceedings{Cav20,
author = {A.~L.~C.~Cavalcanti},
editor = {A.~Raschke and D.~M{\'{e}}ry and F.~Houdek},
title = {{Modelling and Verification of Robotic Platforms for Simulation Using RoboStar Technology}},
booktitle = {Rigorous State-Based Methods - 7th International Conference},
series = {Lecture Notes in Computer Science},
volume = {12071},
pages = {3--5},
publisher = {Springer},
year = {2020},
url = {papers/Cav20.pdf},
doi = {10.1007/978-3-030-48077-6_1}
}
@article{FBCWZ20,
title = {{Unifying semantic foundations for automated verification tools in Isabelle/UTP}},
journal = {Science of Computer Programming},
volume = {197},
year = {2020},
author = {S.~Foster and J.~Baxter and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and F.~Zeyda},
doit = {10.1016/j.scico.2020.102510}
}
@inproceedings{ACW20,
author = {Z.~Attala and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
editor = {A.~Albarghouthi and G.~Katz and N.~Narodytska},
title = {{A Comparison of Neural Network Tools for the Verification of Linear Specifications of ReLU Networks}},
booktitle = {3rd Workshop on Formal Methods for ML-Enabled Autonomous System},
pages = {22--33},
year = {2020},
url = {fomlas2020.wixsite.com/fomlas2020}
}
@article{FYCW21,
author = {S.~Foster and K.~Ye and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock},
title = {Automated verification of reactive and concurrent programs by calculation},
journal = {Journal of Logical and Algebraic Methods in Programming},
volume = {121},
pages = {100681},
year = {2021},
doi = {https://doi.org/10.1016/j.jlamp.2021.100681}
}
@inproceedings{ZDSCCZ21,
author = {M.~Zhang and D.~Du and A.~C.~A.~Sampaio and A.~L.~C.~Cavalcanti and M.~Conserva Filho and M.~Zhang},
title = {{Transforming RoboSim Models into UPPAAL}},
pages = {71--78},
booktitle = {15th International Symposium on Theoretical Aspects of Software Engineering},
publisher = {IEEE},
year = {2021},
doi = {10.1109/TASE.2013.18}
}
@inproceedings{Cav21,
author = {A.~L.~C.~Cavalcanti},
title = {{RoboStar Modelling Stack: Tackling the Reality Gap}},
year = {2021},
publisher = {Association for Computing Machinery},
doi = {10.1145/3459086.3459628},
booktitle = {1st International Workshop on Verification of Autonomous \& Robotic Systems},
series = {VARS 2021}
}
@book{CDHTW21,
editor = {A.~L.~C.~Cavalcanti and B.~Dongol and R.~Hierons and J.~Timmis and J.~C.~P.~Woodcock},
title = {Software Engineering for Robotics},
year = {2021},
publisher = {Springer International Publishing},
isbn = {978-3-030-66493-0},
doi = {10.1007/978-3-030-66494-7}
}
@inbook{CBBCFMRS21,
author = {A.~L.~C.~Cavalcanti and W.~Barnett and J.~Baxter and G.~Carvalho and M.~C.~Filho and A.~Miyazawa and P.~Ribeiro and A.~C.~A.~Sampaio},
editor = {A.~L.~C.~Cavalcanti and B.~Dongol and R.~Hierons and J.~Timmis and J.~C.~P.~Woodcock},
title = {RoboStar Technology: A Roboticist's Toolbox for Combined Proof, Simulation, and Testing},
booktitle = {Software Engineering for Robotics},
year = {2021},
publisher = {Springer International Publishing},
pages = {249--293},
doi = {10.1007/978-3-030-66494-7_9},
url = {papers/CBBCFMRS21.pdf}
}
@inproceedings{CBC21,
author = {A.~L.~C.~Cavalcanti and J.~Baxter and G.~Carvalho},
editor = {R.~Calinescu and C.~S.~P{\u{a}}s{\u{a}}reanu},
title = {RoboWorld: Where Can My Robot Work?},
booktitle = {Software Engineering and Formal Methods},
year = {2021},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
pages = {3--22},
doi = {https://doi.org/10.1007/978-3-030-92124-8_1}
}
@inproceedings{ACJ21,
author = {A.~Abba and A.~L.~C.~Cavalcanti and J.~Jacob},
editor = {S.~Campos and M.~Minea},
title = {{Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata}},
booktitle = {Formal Methods: Foundations and Applications},
year = {2021},
publisher = {Springer},
pages = {70--86},
doi = {https://doi.org/10.1007/978-3-030-92137-8_5}
}
@article{YCFMW22,
author = {K.~Ye and A.~L.~C.~Cavalcanti and S.~Foster and A.~Miyazawa and J.~C.~.P.~Woodcock},
year = {2022},
title = {{Probabilistic modelling and verification using RoboChart and PRISM}},
journal = {Software and Systems Modeling},
doi = {https://doi.org/10.1007/s10270-021-00916-8},
volume = {21},
pages = {667-716}
}
@article{BCM22,
author = {W.~Barnett and A.~L.~C.~Cavalcanti and A.~Miyazawa},
title = {{Architectural Modelling for Robotics: RoboArch and the CorteX example}},
journal = {Frontiers of Robotics and AI},
year = {2022},
doi = {https://doi.org/10.3389/frobt.2022.991637}
}
@inproceedings{WC22,
author = {M.~Windsor and A.~L.~C.~Cavalcanti},
editor = {A.~Riesco and M.~Zhang},
title = {{RoboCert: Property Specification in Robotics}},
booktitle = {International Conference on Formal Engineering Methods},
year = {2022},
publisher = {Springer},
series = {Lecture Notes in Computer Science},
doi = {https://10.1007/978-3-031-17244-1_23},
url = {papers/WC22.pdf},
volume = {13478}
}
@article{MCFDHKLRRTW22,
author = {M.~Mousavi and A.~L.~C.~Cavalcanti and M.~Fisher and L.~Dennis
and R.~Hierons and B.~Kaddouh and E.~L.-C.~Law and R.~Richardson and
J.~O.~Ringert and I.~Tyukin and J.~C.~P.~Woodcock},
title = {{Trustworthy Autonomous Systems through Verifiability}},
journal = {IEEE Software Magazine},
year = {2023},
volume = {56},
number = {2},
doi = {doi.org/10.1109/MC.2022.3192206}
}
@article{BRC22,
title = {{Sound reasoning in tock-CSP}},
journal = {Acta Informatica},
year = {2022},
author = {J.~Baxter and P.~Ribeiro and A.~L.~C.~Cavalcanti},
doi = {10.1007/s00236-020-00394-3},
volume = {59},
pages = {125-162}
}
@article{TPANCCHT22,
title = {{From Pluralistic Normative Principles to Autonomous-Agent Rules}},
journal = {Minds and Machines},
year = {2022},
author = {B.~Townsend and C.~Paterson and T.~T.~Arvind and G.~Nemirovsky and R.~Calinescu and A.~L.~C.~Cavalcanti and I.~Habli and A.~Thomas},
doi = {https://doi.org/10.1007/s11023-022-09614-w}
}
@inproceedings{YBJCC23,
author = {S.~G.~Yaman and C.~Burholt and M.~Jones and R.~Calinescu and A.~L.~C.~Cavalcanti},
editor = {L.~Lambers and S.~Uchitel},
title = {{Specification and Validation of Normative Rules for Autonomous Agents}},
booktitle = {Fundamental Approaches to Software Engineering},
year = {2023},
publisher = {Springer},
doi = {https://doi.org/10.1007/978-3-031-30826-0_13},
volume = {13991}
}
@article{BCGH23,
author = {J.~Baxter and A.~L.~C.~Cavalcanti and M.~Gazda and R.~M.~Hierons},
title = {{Testing Using CSP Models: Time, Inputs, and Outputs}},
year = {2023},
publisher = {Association for Computing Machinery},
volume = {24},
number = {2},
doi = {10.1145/3572837},
journal = {ACM Transactions in Computational Logic}
}
@inbook{CMST23,
author = {A.~L.~C.~Cavalcanti and A.~Miyazawa and U.~Schulze and J.~Timmis},
title = {{Bringing RoboStar and RT-Tester together}},
booktitle = {Jan Peleska's Festschrift},
year = {2023},
publisher = {Springer},
pages = {16--33},
doi = {10.1007/978-3-031-40132-9_2}
}
@inproceedings{CH23,
author = {A.~L.~C.~Cavalcanti and R.~Hierons},
title = {{Challenges in testing cyclic systems}},
booktitle = {27th International Conference on Engineering of Complex Computer Systems},
year = {2023},
publisher = {IEEE}
}
@inproceedings{HCMC23,
author = {H.~Hendry and A.~L.~C.~Cavalcanti and C.~McCall and M.~Chattington},
title = {{Verification of a search-and-rescue drone with humans in the loop}},
booktitle = {14th International Conference on Applied Human Factors and Ergonomics},
year = {2023}
}
@inproceedings{FMYTCCC23,
author = {N.~Feng and L.~Marsso and S.~G.~Yaman and B.~Townsend and A.~L.~C.~Cavalcanti and R.~Calinescu and M.~Chechik},
title = {{Towards a Formal Framework for Normative Requirements Elicitation}},
booktitle = {Automated Software Engineering},
year = {2023},
series = {Conference Publishing Services},
pages = {1776-1780}
}
@article{BCCR23,
author = {J.~Baxter and G.~Carvalho and A.~L.~C.~Cavalcanti and F.~Rodrigues},
title = {{RoboWorld: verification of robotic systems with environment in the loop}},
year = {2023},
publisher = {Association for Computing Machinery},
journal = {Formal Aspects of Computing},
doi = {https://doi.org/10.1145/3625563}
}
@article{MCABPT23,
author = {A.~Miyazawa and A.~L.~C.~Cavalcanti and S.~Ahmadi and J.~Baxter and M.~Post and J.~Timmis},
title = {{Verification with physical models in the loop}},
year = {2023},
publisher = {Springer},
journal = {Systems and Software Modelling},
note = {To appear}
}
@inproceedings{AYDCWM23,
author = {M.~Adam and K.~Ye and D.~Anisi and A.~L.~C.~Cavalcanti and J.~C.~P.~Woodcock and R.~Morris},
title = {{Probabilistic modelling and safety assurance of an agriculture robot providing light-treatment}},
booktitle = {IEEE International Conference on Automation Science and Engineering},
year = {2023}
}
@inproceedings{WCFOSZ23,
author = {J.~C.~P.~Woodcock and A.~L.~C.~Cavalcanti and S.~Foster and M.~V.~M.~Oliveira and A.~C.~A.~Sampaio and F.~Zeyda},
editor = {J.~Bowen and Q.~Li and Q.~Xu},
title = {{UTP, \textsf{\emph{Circus}}, and Isabelle}},
booktitle = {Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday},
year = {2023},
publisher = {Springer},
pages = {19--51},
doi = {10.1007/978-3-031-40436-8_2}
}
@inproceedings{ACW23,
author = {Z.~Attala and A.~L.C.~Cavalcanti and J.~C.~P.~Woodcock},
editor = {E.~{\'A}brah{\'a}m and C.~Dubslaff and S.~L.~T.~Tarifa},
title = {Modelling and Verifying Robotic Software that Uses Neural Networks},
booktitle = {Theoretical Aspects of Computing},
year = {2023},
publisher = {Springer},
pages = {15--35},
doi = {10.1007/978-3-031-47963-2_3}
}
@article{CCRS23,
author = {A.~L.~C.~Cavalcanti and M.~Conserva Filho and P.~Ribeiro and A.~C.A.~Sampaio},
title = {{Laws of Timed State Machines}},
journal = {The Computer Journal},
year = {2023},
doi = {10.1093/comjnl/bxad124}
}
@inproceedings{CABMR23,
author = {A.~L.~C.~Cavalcanti and Z.~Attala and J.~Baxter and A.~Miyazawa and P.~Ribeiro},
editor = {A.~Cerone},
title = {Model-Based Engineering for Robotics with RoboChart and RoboTool},
booktitle = {Formal Methods for an Informal World: ICTAC 2021 Summer School},
year = {2023},
publisher = {Springer International Publishing},
pages = {106--151},
doi = {10.1007/978-3-031-43678-9_4},
url = {https://robostar.cs.york.ac.uk/notations/robochart-tutorial/tutorial.pdf}
}
This file was generated by bibtex2html 1.98.