@article{MTMT:30815533, title = {Theorem and Algorithm Checking for Courses on Logic and Formal Methods}, url = {https://m2.mtmt.hu/api/publication/30815533}, author = {Schreiner, Wolfgang}, doi = {10.4204/EPTCS.290.5}, journal-iso = {ELECTRON PROC THEOR COMPUT SCI}, journal = {ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE}, volume = {290}, unique-id = {30815533}, year = {2019}, eissn = {2075-2180}, pages = {56-75} } @article{MTMT:27191956, title = {A systematic literature review of the use of formal methods in medical software systems}, url = {https://m2.mtmt.hu/api/publication/27191956}, author = {Bonfanti, Silvia and Gargantini, Angelo and Mashkoor, Atif}, doi = {10.1002/smr.1943}, journal-iso = {J SOFTW-EVOL PROC}, journal = {JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS}, volume = {31}, unique-id = {27191956}, issn = {2047-7473}, year = {2018}, eissn = {2047-7481}, pages = {e1943-n/a} } @inproceedings{MTMT:27466940, title = {Validating Mathematical Theorems and Algorithms with RISCAL}, url = {https://m2.mtmt.hu/api/publication/27466940}, author = {Schreiner, Wolfgang}, booktitle = {Intelligent Computer Mathematics}, doi = {10.1007/978-3-319-96812-4_21}, unique-id = {27466940}, abstract = {RISCAL is a language for describing mathematical algorithms and formally specifying their behavior with respect to user-defined theories in first-order logic. This language is based on a type system that constrains the size of all types by formal parameters; thus a RISCAL specification denotes an infinite class of models of which every instance has finite size. This allows the RISCAL software to fully automatically check in small instances the validity of theorems and the correctness of algorithms. Our goal is to quickly detect errors respectively inadequacies in the formalization by falsification in small model instances before attempting actual correctness proofs for the whole model class.}, keywords = {Model checking; falsification; formal specification}, year = {2018}, pages = {248-254} }