TY - JOUR AU - Schreiner, Wolfgang TI - Theorem and Algorithm Checking for Courses on Logic and Formal Methods JF - ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE J2 - ELECTRON PROC THEOR COMPUT SCI VL - 290 PY - 2019 SP - 56 EP - 75 PG - 20 SN - 2075-2180 DO - 10.4204/EPTCS.290.5 UR - https://m2.mtmt.hu/api/publication/30815533 ID - 30815533 LA - English DB - MTMT ER - TY - JOUR AU - Bonfanti, Silvia AU - Gargantini, Angelo AU - Mashkoor, Atif TI - A systematic literature review of the use of formal methods in medical software systems JF - JOURNAL OF SOFTWARE-EVOLUTION AND PROCESS J2 - J SOFTW-EVOL PROC VL - 31 PY - 2018 SP - e1943 EP - n/a SN - 2047-7473 DO - 10.1002/smr.1943 UR - https://m2.mtmt.hu/api/publication/27191956 ID - 27191956 N1 - : Provider: John Wiley & Sons, Ltd : Content:text/plain; charset="UTF-8" Megjegyzés-27201079 : Provider: John Wiley & Sons, Ltd : Content:text/plain; charset="UTF-8" Megjegyzés-27191948 : Provider: John Wiley & Sons, Ltd : Content:text/plain; charset="UTF-8" LA - English DB - MTMT ER - TY - CHAP AU - Schreiner, Wolfgang ED - Rabe, Florian ED - Farmer, William M. ED - Passmore, Grant O. ED - Youssef, Abdou TI - Validating Mathematical Theorems and Algorithms with RISCAL T2 - Intelligent Computer Mathematics PB - Springer Netherlands CY - Cham SN - 9783319968124 T3 - Lecture Notes in Computer Science, ISSN 0302-9743 ; 11006. PY - 2018 SP - 248 EP - 254 PG - 7 DO - 10.1007/978-3-319-96812-4_21 UR - https://m2.mtmt.hu/api/publication/27466940 ID - 27466940 AB - 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. LA - English DB - MTMT ER -