@inproceedings{MTMT:35863943,
	title = {Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem},
	url = {https://m2.mtmt.hu/api/publication/35863943},
	author = {Katsura, H. and Kobayashi, N. and Sakayori, K. and Sato, R.},
	booktitle = {Programming Languages and Systems},
	doi = {10.1007/978-981-97-8943-6_16},
	volume = {15194 LNCS},
	unique-id = {35863943},
	abstract = {A logical approach to automated program verification has been drawing attention recently, where various program verification problems are transformed into formulas of fixpoint logics such as CHC and νHFL(Z), so that a given program satisfies a property just if the corresponding fixpoint formula is valid. In this paper, we show a kind of converse transformation, converting fixpoint logic formulas to programs so that a formula is valid just if the resulting program never evaluates to an (error) value. This, together with the aforementioned transformation from programs to formulas, allows us to go back and forth between logical formulas and programs. In particular, our transformation enables us to use random testing to disprove a given formula, implying that the original program does not satisfy the specified property. As the programs generated by a naive transformation are not suitable for random testing, we employ mode analysis to generate more test-friendly programs. We have implemented the mode-guided transformation and confirmed its effectiveness through experiments. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.},
	keywords = {HYDROGEN-TRANSFER REDUCTIONS; PROPERTY; Logic programming; Software testing; Program Verification; Computer circuits; Reachability problem; random testing; FORTH (programming language); Fixpoints; Logical approaches; Logic formulas; Automated program verification; Mode-based},
	year = {2025},
	pages = {325-345}
}