Logic and Computability Laboratory
Logic and Computability Laboratory
Embedded Files
Research Areas:
Research Areas:
Computability,
Models of Computation,
Complexity, Logic,
Formal Verification, and
Combinatorics
The LCLab focuses on doing computer science on the areas of discrete mathematics, and theories of formal languages, automata, computability and complexity. The current concerns of the group include Computability and Complexity of Nature- and Bio-Inspired Computing Models, Formal Verification of some Algorithms and Cryptographic Protocols, and Discrete Mathematics, Combinatorics and Logic.
The LCLab focuses on doing computer science on the areas of discrete mathematics, and theories of formal languages, automata, computability and complexity. The current concerns of the group include Computability and Complexity of Nature- and Bio-Inspired Computing Models, Formal Verification of some Algorithms and Cryptographic Protocols, and Discrete Mathematics, Combinatorics and Logic.
Research & Projects
Research & Projects
List of Topics of Current Interests of LCLab members, (but not limited to):
List of Topics of Current Interests of LCLab members, (but not limited to):
[If interested, please contact any members of the group for details of the projects/topics listed below]
[If interested, please contact any members of the group for details of the projects/topics listed below]
- Developing a tool that may help colleagues doing formal verification of algorithms of (critical) application systems.
- Formal Verification of some algorithms and possibly cryptographic protocols and some unconventional computing models such as P systems and quantum algorithms.
- Recursion Theory: Application of inductive operator to determine the descriptive complexity of some sets.
- Quantum Complexity, Decoherence: In 2015, we suggested a possibly another way of investigating decoherence of quantum algorithms. I would be interesting to investigate the suggested decoherence measure some quantum optimization algorithms.
- Optimization of quantum computer simulator.
- Topics on Communication complexity, automata and formal languages.
Current Graduate Students Projects
Current Graduate Students Projects
PhD Projects:
PhD Projects:
Communication Complexity in Distributed P Systems with Active Membrane
Kelvin Buno
On Computing with Plasmids
Nestine Hope Hernandez
Master's Project
Master's Project
Adaptive Shot Allocation for Quantum Observable Estimation with Statistical Guarantees
Marc Jermaine Pontiveros
Designing Algorithms and Data Structures for Parallelize Quantum Decision Diagrams for Simulating Quantum Circuit
Jul Jon General [informally with ASTI c/o Jeffrey Aborot]
Formal Verification of ML Models
Jesserey Joseph
Undergrads Project
Undergrads Project
(AY 2025-2026)
(AY 2025-2026)
Lab Special Interest Groups (Lab-SIG):
Lab Special Interest Groups (Lab-SIG):
Formal Verification:
Verification of Deadlock Conditions of xv6 spinlock.c using SPIN Model Checker
Nicholas Reyes and Eoghaine Saavedra
Formal Representation of Kol-Naor Rational Secret Sharing Scheme
Marc Emanuel N. Dela Paz and Keanu Christopher F. Abriol
Recursion Theory:
Extensions and Discussion on Alternative Definitions of Recursive Sets in Models of KPU’
Raniel Emil C. Castro, Sebastian C. Yunque and Marius Barcenas
(AY 2024-2025)
(AY 2024-2025)
Correcting qubit and qutrit errors using Quantum Locally Recoverable Codes made by Hermitian construction. Immanuel Josiah Balete
A measure-once 1-way QFA based on the quantum circuit implementation of a QECC. Julia Dy
Exploring the Use of Finite Field GF(9) in Qutrit Stabilizer Codes for Quantum Error Correction. Kyle David Libiran
Writing a Python-to-CoqTranslator with Automated Theorem Generation. John Ivan Loristo, and Brandon Khalel Martin,
Formal Verification of the Kol and Naor game using COQ. Emilio Capule, Jr., Roberto Joaquin Santos , and Shane Franklin So
(AY 2023-2024)
(AY 2023-2024)
Formal Verification of Round Robin Algorithm Implementation Using Coq. Christian Choa, Brylle Logrono, Raymart Villos
Formal Verification of Shortest Job First Algorithm and Properties in Coq. Jian Luteria, Andrei Tiangco
Formal Verification of FIFO Scheduling Algorithm using Coq Proof Assistant. Earl Wilbur A. Nogra, (Aj Karl A. Valenzuela)
Page updated
Report abuse