Selected publications
Research by Dr. Sam Sammane (published as Ghiath Al Sammane) on symbolic reasoning — formal verification, theorem proving, and decision structures. The 20-year foundation behind QGI's decision-grade platform, organized across three topics: symbolic reasoning, AI & ML, and quantum hypergraph.
- 01
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), 2015.
Consolidated framework for formal verification of AMS designs spanning a decade of collaborative research.
- 02
Automatic Verification of Reduction Techniques in Higher Order Logic
S. Abed, O. Ait Mohamed, G. Al Sammane. Formal Aspects of Computing (Springer), 2013.
Mechanizes correctness proofs for MDG reduction techniques inside HOL, enabling trusted model-checking workflows.
- 03
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, 2009.
Online monitoring technique that catches AMS property violations during simulation rather than post-hoc analysis.
- 04
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, 2009.
Combines HOL-based induction with multiway decision graphs to verify properties over unbounded state spaces.
- 05
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), 2008.
Embeds multiway decision graphs (MDGs) inside the HOL theorem prover to scale reachability analysis beyond pure BDDs.
- 06
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), 2008.
Benchmarks contemporary AMS HDLs — the first systematic performance comparison across VHDL-AMS and Verilog-AMS.
- 07
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), 2007.
Extends the IEEE Property Specification Language (PSL) to analog and mixed-signal designs, enabling assertion-based verification in traditionally simulation-only domains.
- 08
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), 2007.
A symbolic framework for AMS verification that replaces exhaustive simulation with provable coverage of continuous-time behaviors.
- 09
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), 2007.
Combines symbolic simulation with interval arithmetic to bound numerical error when proving AMS properties.
- 10
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), 2007.
Applies runtime verification to phase-locked-loop (PLL) designs — a canonical AMS component difficult to verify statically.
- 11
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), 2007.
Interval-analysis-based constraint verification for delta-sigma modulators, bounding numerical behavior without Monte Carlo.
- 12
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), 2007.
Integrates SAT solving with MDG-based model checking to handle abstract data types outside the reach of pure SAT.
- 13
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), 2007.
High-level abstraction technique that reduces MDG size before reachability analysis, cutting verification time.
- 14
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), 2007.
Formalizes MDG-based reachability inside HOL for trustworthy high-level verification workflows.
- 15
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), 2007.
FPGA emulation platform for comparing digital carrier synchronizer designs used in wireless baseband.
- 16
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), 2007.
Embeds runtime verification directly inside a VHDL-AMS simulator, catching property violations as they occur.
- 17
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), 2005.
Combines symbolic simulation with automatic reasoning to verify behavioral-level hardware descriptions.
- 18
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), 2004.
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.
- 19
Formal Design and Verification of On-Chip Networking
G. A. Sammane, J. Schmaltz, D. Borrione. International Conference on Information and Communication Systems (ICICS), 2004.
Early formal treatment of networks-on-chip (NoC), proving properties of packet routing fabrics.
- 20
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, 2003.
Early work pairing Mathematica symbolic computation with the ACL2 theorem prover for constrained hardware verification.
Dataset: 20 selected publications. Full list on Google Scholar.
Working on related problems?
QGI actively collaborates with researchers on symbolic reasoning, neurosymbolic AI & ML, and quantum hypergraph methods.
Propose a collaboration