Bruda.CA

start - [Teaching]

stefan (stefan@undisclosed.example.com) — 2026-01-03T21:55:02+00:00

Fri 5 Sep 2025 11:18 am -0400		current
Line 18:		Line 18:
	====== Teaching ======		====== Teaching ======

-	This term (Fall 2025) I teach [[http://cs.ubishops.ca/home/cs317\|CS 317 (Design and Analysis of Algorithms)]] and [[http://cs.ubishops.ca/home/cs403\|CS 403 (Principles of Programming Languages)]]	+	This term (Winter 2026) I teach [[http://cs.ubishops.ca/home/cs310\|CS 310 (Introduction to Software Specifications)]] and [[http://cs.ubishops.ca/home/cs464\|CS 464/564 (Network Programming/Network Programming and Distributed Algorithms)]]

	[[teaching\|More...]]		[[teaching\|More...]]

teaching

stefan (stefan@undisclosed.example.com) — 2026-01-03T21:53:17+00:00

Fri 5 Sep 2025 11:17 am -0400		current
Line 1:		Line 1:
	The following are all the undergraduate courses that I teach at Bishop's (some more occasionally than others), together with their most recent Web sites.		The following are all the undergraduate courses that I teach at Bishop's (some more occasionally than others), together with their most recent Web sites.
		+
		+	* [[http://cs.ubishops.ca/home/cs310\|CS 310, Introduction to Software Specifications]] (Winter 2026)
		+	* [[http://cs.ubishops.ca/home/cs464\|CS 464/564, Network Programming/Network Programming and Distributed Algorithms]] (Winter 2026)

	* [[http://cs.ubishops.ca/home/cs317\|CS 317, Design and Analysis of Algorithms]] (Fall 2025)		* [[http://cs.ubishops.ca/home/cs317\|CS 317, Design and Analysis of Algorithms]] (Fall 2025)
	* [[http://cs.ubishops.ca/home/cs403\|CS 403, Principles of Programming Languages]] (Fall 2025)		* [[http://cs.ubishops.ca/home/cs403\|CS 403, Principles of Programming Languages]] (Fall 2025)
-
-	* [[http://cs.ubishops.ca/home/cs310\|CS 310, Introduction to Software Specifications]] (Winter 2025)
	* [[http://cs.ubishops.ca/home/cs467\|CS 467/567, Special/Advanced Topics in Algorithms]] (Winter 2025)		* [[http://cs.ubishops.ca/home/cs467\|CS 467/567, Special/Advanced Topics in Algorithms]] (Winter 2025)
-	* [[http://cs.ubishops.ca/home/cs464\|CS 464/564, Network Programming/Network Programming and Distributed Algorithms]] (Fall 2023)
	* [[http://cs.ubishops.ca/home/cs316\|CS 316, Artificial Intelligence]] (Winter 2023)		* [[http://cs.ubishops.ca/home/cs316\|CS 316, Artificial Intelligence]] (Winter 2023)
	* [[http://cs.ubishops.ca/home/cs455\|CS 455/555, Theoretical Aspects of Computer Science/Automata Theory and Computational Complexity]] (Fall 2020)		* [[http://cs.ubishops.ca/home/cs455\|CS 455/555, Theoretical Aspects of Computer Science/Automata Theory and Computational Complexity]] (Fall 2020)

msc_theses

stefan (stefan@undisclosed.example.com) — 2025-07-26T12:50:51+00:00

Wed 2 Jul 2025 1:07 pm -0400		current
Line 1:		Line 1:
		+	====== On the Equivalence between Must-Test Specifications and the Linear Temporal Logic ======
		+	By Atefeh Farhadi, July 2025. Full paper: {{ :part:farhadi20250711.pdf \|}}
		+
		+	This paper explores the connections between two formal verification techniques: must testing and Linear Temporal Logic (LTL). Both are vital for validating system behaviors and ensuring proper operation. Must testing captures dynamic behaviors and ensures system requirements are met under all execution scenarios, while LTL specifies and verifies temporal properties within systems. Concretely, we explore the equivalence between must testing and LTL. We develop a practical (algorithmic) framework to translate must-test specifications into equivalent LTL formulas. While we thus go only half-way toward establishing an equivalence, we believe that the conversion the other way around is possible as well. On a practical note, we also note that model checking (the algorithmic LTL verification framework) is a very mature technology widely uses in practice, while must testing is deployed to a much lesser extent. We therefore argue that our conversion is much more useful for practical applications. This being said, a conversion of LTL formulae into equivalent must tests is a necessary future expansion of this study to establish formally the equivalence of the two frameworks.
		+
	====== On TorXakis Correctness as an ioco Implementation: An Empirical Model-Based Evaluation ======		====== On TorXakis Correctness as an ioco Implementation: An Empirical Model-Based Evaluation ======
	By Reza Ghasemi, May 2025. Full paper: {{ :part:ghasemi202505.pdf \|}}		By Reza Ghasemi, May 2025. Full paper: {{ :part:ghasemi202505.pdf \|}}

farhadi20250711.pdf - created

stefan (stefan@undisclosed.example.com) — 2025-07-26T12:49:49+00:00

	current

ghasemi202505.pdf - created

stefan (stefan@undisclosed.example.com) — 2025-07-02T17:05:27+00:00

	current

onyeukwu20241210.pdf - created

stefan (stefan@undisclosed.example.com) — 2025-01-06T15:46:49+00:00

	current

teissier-vm.tar.gz

stefan (stefan@undisclosed.example.com) — 2024-10-26T17:37:33+00:00

1430772401	current

run-time_solutions_to_the_stack_overflow_problem

stefan (stefan@undisclosed.example.com) — 2024-10-26T17:30:54+00:00

Fri 13 May 2016 9:12 am -0400		current
Line 3:		Line 3:
	This work is described in the following publication: //Toward Preventing Stack Overflow Using Kernel Properties// (by Benjamin Teissier and Stefan D. Bruda, in Proceedings of the 9th International Conference on Software Engineering and Applications, August 2014, Vienna, Austria).		This work is described in the following publication: //Toward Preventing Stack Overflow Using Kernel Properties// (by Benjamin Teissier and Stefan D. Bruda, in Proceedings of the 9th International Conference on Software Engineering and Applications, August 2014, Vienna, Austria).

-	An [[http://www.ubishops.ca/wp-content/uploads/bucstr-2014-001.pdf\|extended version of this publication]] is available locally. The {{:part:papers:teissier-vm.tar.gz\|code described in the paper}} is also available.	+	An [[http://www.ubishops.ca/wp-content/uploads/bucstr-2014-001.pdf\|extended version of this publication]] is available locally. The {{:part:papers:teissier-vm.tar.gz\|code described in the paper}} is also available under the [[https://www.gnu.org/licenses/\|GNU General Public License]].

	This solution is implemented at the kernel level. A system implementing our method will patch all programs at launch time so that every call and ret will also perform an appropriate system call. As a consequence of the system call attached to calls a copy of the new top of the stack is stored in kernel space. This copy is then compared with the top of the stack stack through the system call associated to ret. This solution is a good proof of concept but is not production ready (see the paper above for a discussion on the matter).		This solution is implemented at the kernel level. A system implementing our method will patch all programs at launch time so that every call and ret will also perform an appropriate system call. As a consequence of the system call attached to calls a copy of the new top of the stack is stored in kernel space. This copy is then compared with the top of the stack stack through the system call associated to ret. This solution is a good proof of concept but is not production ready (see the paper above for a discussion on the matter).
Line 23:		Line 23:
	We also include a fast version that operates in effectively the same manner with the only difference being that it will only verify the stack pointer whenever a write system call is intercepted. This is an approach that attempts to solve the issue of time due to the fact that the full version will check every single instruction and thus takes a significant ammount of time. In order to justify this approach we argue that in practice, we were able to detect that write system calls were issued at key points during the stack overflow and thus, our fast version works under a specific set of conditions.This is further detailed in the thesis.		We also include a fast version that operates in effectively the same manner with the only difference being that it will only verify the stack pointer whenever a write system call is intercepted. This is an approach that attempts to solve the issue of time due to the fact that the full version will check every single instruction and thus takes a significant ammount of time. In order to justify this approach we argue that in practice, we were able to detect that write system calls were issued at key points during the stack overflow and thus, our fast version works under a specific set of conditions.This is further detailed in the thesis.
	==== Files ====		==== Files ====
-	The {{:part:papers:stackintegrityattacks.tar.gz\|complete source code}} is available. The following are the executable programs that constitute our solution:	+	The {{:part:papers:stackintegrityattacks.tar.gz\|complete source code}} is available under the [[https://www.gnu.org/licenses/\|GNU General Public License]]. The following are the executable programs that constitute our solution:

	^ Name ^ Description ^		^ Name ^ Description ^

stackintegrityattacks.tar.gz

stefan (stefan@undisclosed.example.com) — 2024-10-26T17:30:43+00:00

1431296927	current

bahrampour20240428.pdf - created

stefan (stefan@undisclosed.example.com) — 2024-05-01T14:33:33+00:00

	current

publications - [Journal papers]

stefan (stefan@undisclosed.example.com) — 2024-02-07T15:26:13+00:00

Sun 6 Nov 2022 12:21 pm -0500		current
Line 8:		Line 8:

	====== Journal papers ======		====== Journal papers ======
		+	- O. N. Timo, T. Xiao, F. Avellaneda, Y. Malik, and S. Bruda, __Evaluating trustworthiness of decision tree learning algorithms based on equivalence checking__, AI and Ethics (2024), [[https://doi.org/10.1007/s43681-023-00415-0]].
	- C. Huang and S. D. Bruda, [[http://www.acta.sapientia.ro/acta-info/C12-2/info12-2-2.pdf\|Improved balance in multiplayer online battle arena games]], [[http://www.acta.sapientia.ro/acta-info/\|Acta Universitatis Sapientiae, Informatica]], 12:2 (2020) 183-204.		- C. Huang and S. D. Bruda, [[http://www.acta.sapientia.ro/acta-info/C12-2/info12-2-2.pdf\|Improved balance in multiplayer online battle arena games]], [[http://www.acta.sapientia.ro/acta-info/\|Acta Universitatis Sapientiae, Informatica]], 12:2 (2020) 183-204.
	- Mary Sarah Ruth Wilkin and Stefan D. Bruda, [[http://www.acta.sapientia.ro/acta-info/C8-2/info82-01.pdf\|Parallel communicating grammar systems with context-free components are Turing complete for any communication model]], [[http://www.acta.sapientia.ro/acta-info/\|Acta Universitatis Sapientiae, Informatica]], 8:2 (2016), 113−170.		- Mary Sarah Ruth Wilkin and Stefan D. Bruda, [[http://www.acta.sapientia.ro/acta-info/C8-2/info82-01.pdf\|Parallel communicating grammar systems with context-free components are Turing complete for any communication model]], [[http://www.acta.sapientia.ro/acta-info/\|Acta Universitatis Sapientiae, Informatica]], 8:2 (2016), 113−170.

abdolahi20230823.pdf - created

stefan (stefan@undisclosed.example.com) — 2024-01-11T21:52:29+00:00

	current

irannezhadi20230105.pdf - created

stefan (stefan@undisclosed.example.com) — 2023-01-09T00:29:42+00:00

	current

li20220405.pdf - created

stefan (stefan@undisclosed.example.com) — 2022-04-27T18:18:28+00:00

	current

prolog.el

stefan (stefan@undisclosed.example.com) — 2021-09-12T22:44:08+00:00

1631486561	current

omidvar20210502.pdf - created

stefan (stefan@undisclosed.example.com) — 2021-05-18T17:50:17+00:00

	current

xiao20200810.pdf - created

stefan (stefan@undisclosed.example.com) — 2020-08-13T19:42:18+00:00

	current

naserdoust20200413.pdf - created

stefan (stefan@undisclosed.example.com) — 2020-05-23T22:51:51+00:00

	current

nourollahi20191215.pdf - created

stefan (stefan@undisclosed.example.com) — 2020-05-23T22:46:01+00:00

	current

Fri 5 Sep 2025 11:17 am -0400		current
Line 1:		Line 1:
	The following are all the undergraduate courses that I teach at Bishop's (some more occasionally than others), together with their most recent Web sites.		The following are all the undergraduate courses that I teach at Bishop's (some more occasionally than others), together with their most recent Web sites.
		+
		+	* [[http://cs.ubishops.ca/home/cs310\|CS 310, Introduction to Software Specifications]] (Winter 2026)
		+	* [[http://cs.ubishops.ca/home/cs464\|CS 464/564, Network Programming/Network Programming and Distributed Algorithms]] (Winter 2026)

	* [[http://cs.ubishops.ca/home/cs317\|CS 317, Design and Analysis of Algorithms]] (Fall 2025)		* [[http://cs.ubishops.ca/home/cs317\|CS 317, Design and Analysis of Algorithms]] (Fall 2025)
	* [[http://cs.ubishops.ca/home/cs403\|CS 403, Principles of Programming Languages]] (Fall 2025)		* [[http://cs.ubishops.ca/home/cs403\|CS 403, Principles of Programming Languages]] (Fall 2025)
-
-	* [[http://cs.ubishops.ca/home/cs310\|CS 310, Introduction to Software Specifications]] (Winter 2025)
	* [[http://cs.ubishops.ca/home/cs467\|CS 467/567, Special/Advanced Topics in Algorithms]] (Winter 2025)		* [[http://cs.ubishops.ca/home/cs467\|CS 467/567, Special/Advanced Topics in Algorithms]] (Winter 2025)
-	* [[http://cs.ubishops.ca/home/cs464\|CS 464/564, Network Programming/Network Programming and Distributed Algorithms]] (Fall 2023)
	* [[http://cs.ubishops.ca/home/cs316\|CS 316, Artificial Intelligence]] (Winter 2023)		* [[http://cs.ubishops.ca/home/cs316\|CS 316, Artificial Intelligence]] (Winter 2023)
	* [[http://cs.ubishops.ca/home/cs455\|CS 455/555, Theoretical Aspects of Computer Science/Automata Theory and Computational Complexity]] (Fall 2020)		* [[http://cs.ubishops.ca/home/cs455\|CS 455/555, Theoretical Aspects of Computer Science/Automata Theory and Computational Complexity]] (Fall 2020)