Symbolic reasoning
Twenty years of peer-reviewed work on proving — not just testing — that a complex system behaves as specified. Formal verification, theorem proving, and decision structures are the provable core that makes every QGI decision auditable.
Three tracks of symbolic work
Symbolic reasoning at QGI covers formal verification of hardware and neural systems, the decision-graph and theorem-proving machinery that makes verification scale, and the physical-layer simulation and runtime monitoring that keeps deployed systems inside their spec.
Track A
Formal verification of AI & hardware
Reachability bounds, certified robustness, and assertion-based verification — originally built for analog, mixed-signal, and digital hardware, now extended to neural networks and regulated decision systems. Includes PSL-style property languages, interval arithmetic, and symbolic simulation.
Track B
Decision structures & theorem proving
Multiway Decision Graphs (MDGs) inside HOL, SAT/SMT integration, and machine-checked proofs of reduction correctness. The infrastructure that makes "prove this AI decision is within the policy" tractable at production scale — not just on toy examples.
Track C
Simulation, circuits & runtime monitoring
Symbolic simulation, VHDL-AMS runtime verification, networks-on-chip, delta-sigma modulators, and online monitoring. The physical-layer half of the story: how symbolic guarantees ride into deployed systems, and how property violations are caught before they become incidents.
20 peer-reviewed papers
- 2015 chapter
Framework for Formally Verifying Analog and Mixed-Signal Designs
M. H. Zaki, O. Hasan, S. Tahar, G. Al-Sammane. Computational Intelligence in AMS and Radio-Frequency Circuits (Springer).
Consolidated framework for formal verification of AMS designs spanning a decade of collaborative research.
View on Google Scholar - 2013 journal
Automatic Verification of Reduction Techniques in Higher Order Logic
S. Abed, O. Ait Mohamed, G. Al Sammane. Formal Aspects of Computing (Springer).
Mechanizes correctness proofs for MDG reduction techniques inside HOL, enabling trusted model-checking workflows.
View on Google Scholar - 2009 workshop
Verification of Analog and Mixed Signal Designs Using Online Monitoring
Z. Wang, N. Abbasi, R. Narayanan, M. H. Zaki, G. Al Sammane, S. Tahar. IEEE International Mixed-Signals, Sensors, and Systems Test Workshop.
Online monitoring technique that catches AMS property violations during simulation rather than post-hoc analysis.
View on Google Scholar - 2009 journal
An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs
S. Abed, O. A. Mohamed, G. Al-Sammane. Journal of Computer Science and Technology.
Combines HOL-based induction with multiway decision graphs to verify properties over unbounded state spaces.
View on Google Scholar - 2008 conference
Reachability Analysis Using Multiway Decision Graphs in the HOL Theorem Prover
S. Abed, O. Ait Mohamed, G. Al Sammane. ACM Symposium on Applied Computing (SAC).
Embeds multiway decision graphs (MDGs) inside the HOL theorem prover to scale reachability analysis beyond pure BDDs.
View on Google Scholar - 2008 conference
On the Simulation Performance of Contemporary AMS Hardware Description Languages
R. Narayanan, N. Abbasi, M. Zaki, G. Al Sammane, S. Tahar. International Conference on Microelectronics (ICM).
Benchmarks contemporary AMS HDLs — the first systematic performance comparison across VHDL-AMS and Verilog-AMS.
View on Google Scholar - 2007 conference 47 citations
Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL
G. Al Sammane, M. H. Zaki, Z. J. Dong, S. Tahar. Forum on Specification and Design Languages (FDL).
Extends the IEEE Property Specification Language (PSL) to analog and mixed-signal designs, enabling assertion-based verification in traditionally simulation-only domains.
View on Google Scholar - 2007 conference 44 citations
A Symbolic Methodology for the Verification of Analog and Mixed Signal Designs
G. Al-Sammane, M. H. Zaki, S. Tahar. Design, Automation & Test in Europe (DATE).
A symbolic framework for AMS verification that replaces exhaustive simulation with provable coverage of continuous-time behaviors.
View on Google Scholar - 2007 conference
Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs
M. H. Zaki, G. Al-Sammane, S. Tahar, G. Bois. Formal Methods in Computer Aided Design (FMCAD).
Combines symbolic simulation with interval arithmetic to bound numerical error when proving AMS properties.
View on Google Scholar - 2007 conference
Checking Properties of PLL Designs Using Run-Time Verification
Z. J. Dong, M. H. Zaki, G. Al Sammane, S. Tahar, G. Bois. International Conference on Microelectronics (ICM).
Applies runtime verification to phase-locked-loop (PLL) designs — a canonical AMS component difficult to verify statically.
View on Google Scholar - 2007 conference
Constraint-Based Verification of Delta-Sigma Modulators Using Interval Analysis
G. Al Sammane, M. H. Zaki, S. Tahar, G. Bois. IEEE Midwest Symposium on Circuits and Systems (MWSCAS).
Interval-analysis-based constraint verification for delta-sigma modulators, bounding numerical behavior without Monte Carlo.
View on Google Scholar - 2007 conference
Integrating SAT with Multiway Decision Graphs for Efficient Model Checking
S. Abed, O. Ait Mohamed, Z. Yang, G. Al Sammane. International Conference on Microelectronics (ICM).
Integrates SAT solving with MDG-based model checking to handle abstract data types outside the reach of pure SAT.
View on Google Scholar - 2007 workshop
High-Level Reduction Technique for Multiway Decision Graphs Based Model Checking
G. A. Sammane, S. Abed, O. A. Mohamed. Verification and Evaluation of Computer and Communication Systems (VECoS).
High-level abstraction technique that reduces MDG size before reachability analysis, cutting verification time.
View on Google Scholar - 2007 conference
A High-Level Reachability Analysis Using Multiway Decision Graphs in the HOL Theorem Prover
S. Abed, O. Ait Mohamed, G. Al Sammane. Theorem Proving in Higher Order Logics (TPHOLs).
Formalizes MDG-based reachability inside HOL for trustworthy high-level verification workflows.
View on Google Scholar - 2007 workshop
FPGA Emulation Environment of Different Digital Carrier Synchronizers
A. I. Ahmed, S. H. Rahman, G. Al-Sammane, O. Ait Mohamed. IEEE Northeast Workshop on Circuits and Systems (NEWCAS).
FPGA emulation platform for comparing digital carrier synchronizer designs used in wireless baseband.
View on Google Scholar - 2007 workshop
Run-Time Verification Using the VHDL-AMS Simulation Environment
Z. J. Dong, M. H. Zaki, G. Al Sammane, S. Tahar, G. Bois. IEEE Northeast Workshop on Circuits and Systems (NEWCAS).
Embeds runtime verification directly inside a VHDL-AMS simulator, catching property violations as they occur.
View on Google Scholar - 2005 conference
Verification of Behavioral Descriptions by Combining Symbolic Simulation and Automatic Reasoning
G. Al Sammane, D. Borrione, R. Chevallier. ACM Great Lakes Symposium on VLSI (GLSVLSI).
Combines symbolic simulation with automatic reasoning to verify behavioral-level hardware descriptions.
View on Google Scholar - 2004 conference
TheoSim: Combining Symbolic Simulation and Theorem Proving for Hardware Verification
G. Al Sammane, J. Schmaltz, D. Toma, P. Ostier, D. Borrione. Symposium on Integrated Circuits and System Design (SBCCI).
The TheoSim framework — foundational work unifying symbolic simulation with theorem proving for hardware verification. Forms the theoretical basis for combining neural simulation with symbolic reasoning under a single verification regime.
View on Google Scholar - 2004 conference
Formal Design and Verification of On-Chip Networking
G. A. Sammane, J. Schmaltz, D. Borrione. International Conference on Information and Communication Systems (ICICS).
Early formal treatment of networks-on-chip (NoC), proving properties of packet routing fabrics.
View on Google Scholar - 2003 conference
Constrained Symbolic Simulation with Mathematica and ACL2
G. Al Sammane, D. Toma, J. Schmaltz, P. Ostier, D. Borrione. CHARME — Correct Hardware Design and Verification Methods.
Early work pairing Mathematica symbolic computation with the ACL2 theorem prover for constrained hardware verification.
View on Google Scholar
Working on formal methods for neural systems, HOL/Lean/Coq, or SAT/SMT at scale?