@article(a20a,
 author       = {Cinzia Bernardeschi and Pierpaolo Dini and Andrea Domenici and Maurizio Palmieri and Sergio Saponara},
 year         = {2020},
 title        = {Formal Verification and Co-Simulation in the Design of a Synchronous Motor Control Algorithm},
 journal      = {Energies},
 volume       = {13},
 number       = {16},
 pages        = {4057},
 doi          = {10.3390/en13164057},
)
@inproceedings(a18,
 author       = {Andrea Domenici and Adriano Fagiolini and Maurizio Palmieri},
 year         = {2018},
 title        = {Integrated Simulation and Formal Verification of a Simple Autonomous Vehicle},
 editor       = {Antonio Cerone and Marco Roveri},
 booktitle    = {Software Engineering and Formal Methods},
 series       = {Lecture Notes in Computer Science},
 volume       = {10729},
 publisher    = {Springer International Publishing},
 address      = {Cham},
 pages        = {300--314},
 doi          = {10.1007/978-3-319-74781-1\_21},
)
@incollection(dutertre96,
 author       = {Bruno Dutertre},
 year         = {1996},
 title        = {{Elements of mathematical analysis in PVS}},
 editor       = {Gerhard Goos and Juris Hartmanis and Jan van Leeuwen and Joakim von Wright and Jim Grundy and John Harrison},
 booktitle    = {Theorem Proving in Higher Order Logics},
 series       = {Lecture Notes in Computer Science},
 volume       = {1125},
 publisher    = {Springer Berlin Heidelberg},
 pages        = {141--156},
 doi          = {10.1007/BFb0105402},
)
@incollection(owre96,
 author       = {S. Owre and S. Rajan and J. Rushby and N. Shankar and M. Srivas},
 year         = {1996},
 title        = {{PVS: combining specification, proof checking, and model checking}},
 editor       = {R. Alur and T.A. Henzinger},
 booktitle    = {Computer-Aided Verification, CAV '96},
 series       = {LNCS},
 volume       = {1102},
 publisher    = {Springer-Verlag},
 pages        = {411--414},
 doi          = {10.1007/3-540-61474-5\_91},
)
@book(slotine91,
 author       = {J. E. Slotine and W. Li},
 year         = {1991},
 title        = {Applied Nonlinear Control},
 publisher    = {Prentice-Hall},
 address      = {Englewood Cliffs, NJ},
)
@book(smullyan68,
 author       = {Raymond Merrill Smullyan},
 year         = {1968},
 title        = {First-order logic},
 series       = {Ergebnisse der Mathematik und ihrer Grenzgebiete},
 publisher    = {Springer, Berlin, Heidelberg},
 doi          = {10.1007/978-3-642-86718-7},
)